1.1.数学证明¶

1.1. Mathematical Proof¶

尽管有书面证据表明早在公元前 3000 年埃及就出现了数学活动，但许多学者认为真正的数学诞生于公元前六世纪左右的古希腊，当时首次引入了演绎证明。亚里士多德认为米利都的泰勒斯不仅认识到了我们所知道的东西的重要性，而且认识到了我们如何知道的重要性，并在演绎方法中找到了知识的基础。公元前 300 年左右，欧几里得在他的论文《几何原本》中编纂了几何学的演绎方法。几个世纪以来，欧几里得的公理化风格被视为严格论证的典范，不仅在数学中，而且在哲学和科学中也是如此。

Although there is written evidence of mathematical activity in Egypt as early as 3000 BC, many scholars locate the birth of mathematics proper in ancient Greece around the sixth century BC, when deductive proof was first introduced. Aristotle credited Thales of Miletus with recognizing the importance of not just what we know but how we know it, and finding grounds for knowledge in the deductive method. Around 300 BC, Euclid codified a deductive approach to geometry in his treatise, the Elements. Through the centuries, Euclid’s axiomatic style was held as a paradigm of rigorous argumentation, not just in mathematics, but in philosophy and the sciences as well.

这是一个用当代数学语言来表达的普通证明的例子。它证实了毕达哥拉斯学派所知道的一个事实。

Here is an example of an ordinary proof, in contemporary mathematical language. It establishes a fact that was known to the Pythagoreans.

定理。 $\sqrt{2}$是无理数，也就是说，它不能用分数来表示$a/b$， 在哪里$a$和$b$是整数。

Theorem. $\sqrt{2}$ is irrational, which is to say, it cannot be expressed as a fraction $a/b$, where $a$ and $b$ are integers.

证明。假设$\sqrt{2}=a/b$对于某对整数$a$和$b$。通过消除所有共同因素，我们可以假设$a/b$是最低的，因此$a$和$b$没有共同的因素。那么我们有$a=\sqrt{2}b$，然后对两边取平方，可得$a^2=2b^2$。

Proof. Suppose $\sqrt{2}=a/b$ for some pair of integers $a$ and $b$. By removing any common factors, we can assume $a/b$ is in lowest terms, so that $a$ and $b$ have no factor in common. Then we have $a=\sqrt{2}b$, and squaring both sides, we have $a^2=2b^2$.

最后一个等式意味着$a^2$是偶数，而奇数的平方也是奇数，$a$本身也必定是偶数。因此我们有$a=2c$对于某个整数$c$. 将其代入方程$a^2=2b^2$，我们有$4c^2=2b^2$，因此$2c^2=b^2$.这意味着$b^2$是偶数，所以$b$也同样如此。

The last equation implies that $a^2$ is even, and since the square of an odd number is odd, $a$ itself must be even as well. We therefore have $a=2c$ for some integer $c$. Substituting this into the equation $a^2=2b^2$, we have $4c^2=2b^2$, and hence $2c^2=b^2$. This means that $b^2$ is even, and so $b$ is even as well.

事实是$a$和$b$甚至与以下事实相矛盾：$a$和$b$没有共同因素。因此最初的假设$\sqrt{2}=a/b$是错误的。

The fact that $a$ and $b$ are both even contradicts the fact that $a$ and $b$ have no common factor. So the original assumption that $\sqrt{2}=a/b$ is false.

在下一个例子中，我们关注自然数，

In the next example, we focus on the natural numbers,

自然数$n$如果大于或等于 2，则称其为合数，如果它可以写成乘积$n=m\cdot k$既不$m$也不$k$等于$1$，否则为素数。注意如果$n=m\cdot k$见证了这一事实$n$是复合的，那么$m$和$k$都小于$n$还要注意，按照惯例，0 和 1 既不被视为质数也不被视为合数。

A natural number $n$ greater than or equal to 2 is said to be composite if it can be written as a product $n=m\cdot k$ where neither $m$ nor $k$ is equal to $1$, and prime otherwise. Notice that if $n=m\cdot k$ witnesses the fact that $n$ is composite, then $m$ and $k$ are both smaller than $n$. Notice also that, by convention, 0 and 1 are considered neither prime nor composite.

定理。每个大于或等于 2 的自然数都可以写成素数的乘积。

Theorem. Every natural number greater than or equal to 2 can be written as a product of primes.

证明。我们通过归纳法进行$n$。 让$n$为大于 2 的任意自然数。如果$n$是素数，我们就完成了；我们可以考虑$n$本身就是一个项的乘积。否则，$n$是复合的，我们可以写成$n=m\cdot k$在哪里$m$和$k$小于$n$并且大于 1。根据归纳假设，$m$和$k$可以写成素数的乘积，比如 $m=p_1\cdot p_2\cdot \dots \cdot p_u$和$k=q_1\cdot q_2\cdot \dots \cdot q_v$.但随后我们有

Proof. We proceed by induction on $n$. Let $n$ be any natural number greater than 2. If $n$ is prime, we are done; we can consider $n$ itself as a product with one term. Otherwise, $n$ is composite, and we can write $n=m\cdot k$ where $m$ and $k$ are smaller than $n$ and greater than 1. By the inductive hypothesis, each of $m$ and $k$ can be written as a product of primes, say $m=p_1\cdot p_2\cdot \dots \cdot p_u$ and $k=q_1\cdot q_2\cdot \dots \cdot q_v$. But then we have

根据需要，素数的乘积。

a product of primes, as required.

稍后，我们将看到更多的事实是真实的：每一个大于 2 的自然数都可以用独特的方式写成素数的乘积，这一事实被称为算术基本定理。

Later, we will see that more is true: every natural number greater than 2 can be written as a product of primes in a unique way, a fact known as the fundamental theorem of arithmetic.

本课程的首要目标是教您编写清晰易读的数学证明。我们将通过考虑大量示例来实现这一目标，同时也采取反思的观点：我们将仔细研究数学语言的组成部分和数学证明的结构，以便更好地理解它们的工作原理。

The first goal of this course is to teach you to write clear, readable mathematical proofs. We will do this by considering a number of examples, but also by taking a reflective point of view: we will carefully study the components of mathematical language and the structure of mathematical proofs, in order to gain a better understanding of how they work.

1.2.符号逻辑¶

1.2. Symbolic Logic¶

为了理解证明的工作原理，研究“符号逻辑”这一主题将大有裨益，它提供了数学语言和证明的理想模型。在《前分析篇》中，这位古希腊哲学家着手分析推理模式，并发展了三段论理论。以下是三段论的一个例子：

Toward understanding how proofs work, it will be helpful to study a subject known as “symbolic logic,” which provides an idealized model of mathematical language and proof. In the Prior Analytics, the ancient Greek philosopher set out to analyze patterns of reasoning, and developed the theory of the syllogism. Here is one instance of a syllogism:

每个人都是动物。

Every man is an animal.

任何动物都会死。

Every animal is mortal.

因此，每个人都终有一死。

Therefore every man is mortal.

亚里士多德指出，这种推论的正确性与个别陈述的真实性或虚假性无关，而是与一般模式有关：

Aristotle observed that the correctness of this inference has nothing to do with the truth or falsity of the individual statements, but, rather, the general pattern:

每个 A 都是 B。

Every A is B.

每个 B 都是 C。

Every B is C.

因此每个 A 都是 C。

Therefore every A is C.

我们可以用各种属性来代替 A、B 和 C；试着用鱼、独角兽、游泳生物、神话生物等属性来代替。由此产生的各种陈述可能为真或为假，但所有实例都具有以下关键特征：如果两个假设为真，则结论也为真。我们通过说推理有效来表达这一点。

We can substitute various properties for A, B, and C; try substituting the properties of being a fish, being a unicorn, being a swimming creature, being a mythical creature, etc. The various statements that result may come out true or false, but all the instantiations will have the following crucial feature: if the two hypotheses come out true, then the conclusion comes out true as well. We express this by saying that the inference is valid.

尽管亚里士多德的推理理论所针对的语言模式有限，但我们仍要感谢他提出的一个关键洞见：我们可以根据逻辑形式对有效的推理模式进行分类，同时抽象出具体内容。这一基本观察是整个符号逻辑领域的基础。

Although the patterns of language addressed by Aristotle’s theory of reasoning are limited, we have him to thank for a crucial insight: we can classify valid patterns of inference by their logical form, while abstracting away specific content. It is this fundamental observation that underlies the entire field of symbolic logic.

17 世纪，莱布尼茨提出了“普遍性”的设计，这是一种通用的符号语言，人们可以用它精确地表达任何断言，以及“推理演算”，这是一种“思维演算”，可以表达精确的推理规则。莱布尼茨自己也采取了一些措施来开发这种语言和演算，但更大的进步是在 19 世纪取得的，这要归功于布尔、弗雷格、皮尔斯、施罗德等人的努力。20 世纪初，这些努力在数理逻辑领域蓬勃发展。

In the seventeenth century, Leibniz proposed the design of a characteristica universalis, a universal symbolic language in which one would express any assertion in a precise way, and a calculus ratiocinatur, a “calculus of thought” which would express the precise rules of reasoning. Leibniz himself took some steps to develop such a language and calculus, but much greater strides were made in the nineteenth century, through the work of Boole, Frege, Peirce, Schroeder, and others. Early in the twentieth century, these efforts blossomed into the field of mathematical logic.

如果您考虑上一节中的证明示例，您会注意到一些术语和推理规则特定于当前主题，与数字以及质数、合数、偶数、奇数等属性有关。但还有其他术语和推理规则并非特定于领域，例如与“每个”、“一些”、“和”和“如果……那么”等词相关的术语和规则。符号逻辑的目标是识别这些推理和论证的核心要素并解释它们的工作原理，以及解释如何引入和使用更多特定领域的概念。

If you consider the examples of proofs in the last section, you will notice that some terms and rules of inference are specific to the subject matter at hand, having to do with numbers and the properties of being prime, composite, even, odd, and so on. But there are other terms and rules of inference that are not domain specific, such as those related to the words “every,” “some,” “and,” and “if … then.” The goal of symbolic logic is to identify these core elements of reasoning and argumentation and explain how they work, as well as to explain how more domain-specific notions are introduced and used.

为此，我们将引入关键逻辑概念的符号，包括以下内容：

To that end, we will introduce symbols for key logical notions, including the following:

• $A\to B$，“$\text{if }A\text{ then }B$”

• $A\to B$, “$\text{if }A\text{ then }B$”

• $A\wedge B$，“$A\text{ and }B$”

• $A\wedge B$, “$A\text{ and }B$”

• $A\vee B$，“$A\text{ or }B$”

• $A\vee B$, “$A\text{ or }B$”

• $\mathrm{\neg }A$，“$\text{not }A$”

• $\mathrm{\neg }A$, “$\text{not }A$”

• $\mathrm{\forall }xA$，“$\text{for every }x\text{, }A$”

• $\mathrm{\forall }xA$, “$\text{for every }x\text{, }A$”

• $\mathrm{\exists }xA$，“$\text{for some }x\text{, }A$”

• $\mathrm{\exists }xA$, “$\text{for some }x\text{, }A$”

然后，我们将提供一个正式的证明系统，让我们通过演绎的方式证明这些陈述之间的某些蕴涵是有效的。

We will then provide a formal proof system that will let us establish, deductively, that certain entailments between such statements are valid.

我们将使用的证明系统是自然演绎法的一种，这是 Gerhard Gentzen 在 20 世纪 30 年代引入的一种证明系统，用于模拟非正式论证风格。在这个系统中，判断的基本单位是断言一个陈述，$A$，根据一组有限的假设，$\mathrm{\Gamma }$. 写为$\mathrm{\Gamma }⊢A$。 如果$\mathrm{\Gamma }$和$\mathrm{\Delta }$是两个有限的假设集，我们将写成$\mathrm{\Gamma },\mathrm{\Delta }$表示这两个集合的并集，即由每个集合中的所有假设组成的集合。根据这些约定，合取符号的规则可以表示如下：

The proof system we will use is a version of natural deduction, a type of proof system introduced by Gerhard Gentzen in the 1930s to model informal styles of argument. In this system, the fundamental unit of judgment is the assertion that a statement, $A$, follows from a finite set of hypotheses, $\mathrm{\Gamma }$. This is written as $\mathrm{\Gamma }⊢A$. If $\mathrm{\Gamma }$ and $\mathrm{\Delta }$ are two finite sets of hypotheses, we will write $\mathrm{\Gamma },\mathrm{\Delta }$ for the union of these two sets, that is, the set consisting of all the hypotheses in each. With these conventions, the rule for the conjunction symbol can be expressed as follows:

这应该被理解为：假设$A$根据假设$\mathrm{\Gamma }$， 和$B$根据假设$\mathrm{\Delta }$，$A\wedge B$根据这两个假设$\mathrm{\Gamma }$和$\mathrm{\Delta }$。

This should be interpreted as saying: assuming $A$ follows from the hypotheses $\mathrm{\Gamma }$, and $B$ follows from the hypotheses $\mathrm{\Delta }$, $A\wedge B$ follows from the hypotheses in both $\mathrm{\Gamma }$ and $\mathrm{\Delta }$.

我们将看到，人们可以更紧凑地写出这样的证明，而隐含假设，这样上面的规则就可以表达如下：

We will see that one can write such proofs more compactly leaving the hypotheses implicit, so that the rule above is expressed as follows:

在这种格式中，上一节中第一个证明的片段可能呈现如下：

In this format, a snippet of the first proof in the previous section might be rendered as follows:

此类证明的复杂性很快就会变得无法控制，即使是基本数学事实的完整证明也会变得相当冗长。此类系统并非为编写严肃的数学而设计。相反，它们提供了理想化的数学推理模型，只要它们捕捉到某种非正式证明的结构，它们就使我们能够研究数学推理的性质。

The complexity of such proofs can quickly grow out of hand, and complete proofs of even elementary mathematical facts can become quite long. Such systems are not designed for writing serious mathematics. Rather, they provide idealized models of mathematical inference, and insofar as they capture something of the structure of an informal proof, they enable us to study the properties of mathematical reasoning.

本课程的第二个目标是帮助您理解自然演绎，作为正式演绎系统的一个示例。

The second goal of this course is to help you understand natural deduction, as an example of a formal deductive system.

1.3.交互式定理证明¶

1.3. Interactive Theorem Proving¶

数理逻辑的早期研究旨在表明，至少在原则上，普通数学论证可以用符号演算建模。如上所述，复杂性问题限制了实践中可以实现的范围；即使是基本的数学论证也需要很长的推导过程，这些推导过程很难写，也很难读，而且对促进对底层数学的理解几乎没有帮助。

Early work in mathematical logic aimed to show that ordinary mathematical arguments could be modeled in symbolic calculi, at least in principle. As noted above, complexity issues limit the range of what can be accomplished in practice; even elementary mathematical arguments require long derivations that are hard to write and hard to read, and do little to promote understanding of the underlying mathematics.

然而，自 20 世纪末以来，计算证明助手的出现开始使完全形式化成为可能。通过与定理证明软件交互，用户可以构建复杂定理的形式化推导，这些推导可以由计算机存储和检查。自动化方法可用于手动填补小空白、公理化地验证长计算或确定性地填充长推理链。然而，自动化的范围目前相当有限。交互式定理证明中使用的策略是要求用户提供足够的信息，以便系统能够构建和检查形式化推导。这通常涉及用一种为此目的而设计的“编程语言”编写证明。例如，这是Lean定理证明器中的一个简短证明：

Since the end of the twentieth century, however, the advent of computational proof assistants has begun to make complete formalization feasible. Working interactively with theorem proving software, users can construct formal derivations of complex theorems that can be stored and checked by computer. Automated methods can be used to fill in small gaps by hand, verify long calculations axiomatically, or fill in long chains of inferences deterministically. The reach of automation is currently fairly limited, however. The strategy used in interactive theorem proving is to ask users to provide just enough information for the system to be able to construct and check a formal derivation. This typically involves writing proofs in a sort of “programming language” that is designed with that purpose in mind. For example, here is a short proof in the Lean theorem prover:

section
variables (P Q : Prop)

theorem my_theorem : P ∧ Q → Q ∧ P :=
assume h : P ∧ Q,
have P, from and.left h,
have Q, from and.right h,
show Q ∧ P, from and.intro ‹Q› ‹P›

end

section
variables (P Q : Prop)

theorem my_theorem : P ∧ Q → Q ∧ P :=
assume h : P ∧ Q,
have P, from and.left h,
have Q, from and.right h,
show Q ∧ P, from and.intro ‹Q› ‹P›

end

如果您以在线形式阅读当前文本，您会在正式的“证明脚本”上方看到一个按钮，上面写着“试试看！”按下该按钮会在编辑器窗口中打开证明，并在浏览器中运行 Lean 版本来处理证明，将其转换为公理推导，并验证其正确性。您可以通过改变编辑器中的文本进行实验；任何错误都会在右侧窗口中注明。

If you are reading the present text in online form, you will find a button above the formal “proof script” that says “try it!” Pressing the button opens the proof in an editor window and runs a version of Lean inside your browser to process the proof, turn it into an axiomatic derivation, and verify its correctness. You can experiment by varying the text in the editor; any errors will be noted in the window to the right.

Lean 中的证明可以访问先前的数学结果库，所有结果都经过公理基础验证。交互式定理证明领域的一个目标是达到任何当代定理都可以通过这种方式验证的程度。例如，下面是一个正式证明，证明二的平方根是无理数，遵循上面提出的非正式证明的模型：

Proofs in Lean can access a library of prior mathematical results, all verified down to axiomatic foundations. A goal of the field of interactive theorem proving is to reach the point where any contemporary theorem can be verified in this way. For example, here is a formal proof that the square root of two is irrational, following the model of the informal proof presented above:

import data.nat.prime
open nat

theorem sqrt_two_irrational {a b : ℕ} (co : gcd a b = 1) :
  a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
  by simp [h],
have 2 ∣ a,
  from prime.dvd_of_dvd_pow prime_two this,
exists.elim this $
assume (c : nat) (aeq : a = 2 * c),
have 2 * (2 * c^2) = 2 * b^2,
  by simp [eq.symm h, aeq];
    simp [pow_succ', mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
  from mul_left_cancel' dec_trivial this,
have 2 ∣ b^2,
  by simp [eq.symm this],
have 2 ∣ b,
  from prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
  from dvd_gcd ‹2 ∣ a› ‹2 ∣ b›,
have 2 ∣ (1 : ℕ),
  by simp * at *,
show false, from absurd ‹2 ∣ 1› dec_trivial

import data.nat.prime
open nat

theorem sqrt_two_irrational {a b : ℕ} (co : gcd a b = 1) :
  a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
  by simp [h],
have 2 ∣ a,
  from prime.dvd_of_dvd_pow prime_two this,
exists.elim this $
assume (c : nat) (aeq : a = 2 * c),
have 2 * (2 * c^2) = 2 * b^2,
  by simp [eq.symm h, aeq];
    simp [pow_succ', mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
  from mul_left_cancel' dec_trivial this,
have 2 ∣ b^2,
  by simp [eq.symm this],
have 2 ∣ b,
  from prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
  from dvd_gcd ‹2 ∣ a› ‹2 ∣ b›,
have 2 ∣ (1 : ℕ),
  by simp * at *,
show false, from absurd ‹2 ∣ 1› dec_trivial

本课程的第三个目标是教您用精益语言编写基本证明。我们要求您在精益语言中证明的事实将比我们要求您编写的非正式证明更基本，但我们的目的是正式证明将模拟和阐明我们将教给您的非正式证明策略。

The third goal of this course is to teach you to write elementary proofs in Lean. The facts that we will ask you to prove in Lean will be more elementary than the informal proofs we will ask you to write, but our intent is that formal proofs will model and clarify the informal proof strategies we will teach you.

1.4.语义观点¶

1.4. The Semantic Point of View¶

正如我们在此介绍的主题，符号逻辑的目标是指定一种语言和推理规则，使我们能够以可靠的方式获得真相。这个想法是，我们选择的符号表示具有固定含义的对象和概念，我们采用的推理规则使我们能够从真实的假设中得出真实的结论。

As we have presented the subject here, the goal of symbolic logic is to specify a language and rules of inference that enable us to get at the truth in a reliable way. The idea is that the symbols we choose denote objects and concepts that have a fixed meaning, and the rules of inference we adopt enable us to draw true conclusions from true hypotheses.

然而，人们可以采用另一种观点来看待逻辑，即逻辑是一个系统，其中某些符号具有固定的含义，例如“与”、“或”和“非”的符号，而其他符号的含义可以变化。例如，表达式$P\wedge (Q\vee R)$， 读 ”$P$并且要么$Q$或者$R$”可能为真也可能为假，这取决于以下基本断言 $P$，$Q$，和 $R$ 代表。更准确地说，复合表达式的真值仅取决于组成符号表示的表达式是真还是假。例如，如果$P$，$Q$， 和$R$分别代表“七是质数”、“七是偶数”和“七是奇数”，则表达式为真。如果我们用“六”代替“七”，则该语句为假。更一般地，只要$P$是真的，并且至少有一个$Q$和$R$为真，否则为假。

One can adopt another view of logic, however, as a system where some symbols have a fixed meaning, such as the symbols for “and,” “or,” and “not,” and others have a meaning that is taken to vary. For example, the expression $P\wedge (Q\vee R)$, read “$P$ and either $Q$ or $R$,” may be true or false depending on the basic assertions that $P$, $Q$, and $R$ stand for. More precisely, the truth of the compound expression depends only on whether the component symbols denote expressions that are true or false. For example, if $P$, $Q$, and $R$ stand for “seven is prime,” “seven is even,” and “seven is odd,” respectively, then the expression is true. If we replace “seven” by “six,” the statement is false. More generally, the expression comes out true whenever $P$ is true and at least one of $Q$ and $R$ is true, and false otherwise.

从这个角度来看，逻辑与其说是一种断言真理的语言，不如说是一种描述可能事态的语言。换句话说，逻辑提供了一种规范语言，表达式可以是真或假，这取决于我们如何解释允许变化的符号。例如，如果我们固定了基本谓词的含义，那么“两个蓝色块之间有一个红色块”这个陈述在给定的块“世界”中可能是真或假，我们可以用这个表达式来描述它为真的世界集。这种逻辑观在计算机科学中很重要，我们使用逻辑表达式从数据库中选择符合某些标准的条目，指定硬件和软件系统的属性，或者断言我们希望约束求解器满足的约束。

From this perspective, logic is not so much a language for asserting truth, but a language for describing possible states of affairs. In other words, logic provides a specification language, with expressions that can be true or false depending on how we interpret the symbols that are allowed to vary. For example, if we fix the meaning of the basic predicates, the statement “there is a red block between two blue blocks” may be true or false of a given “world” of blocks, and we can take the expression to describe the set of worlds in which it is true. Such a view of logic is important in computer science, where we use logical expressions to select entries from a database matching certain criteria, to specify properties of hardware and software systems, or to assert constraints that we would like a constraint solver to satisfy.

一方面，句法 / 演绎观点与另一方面的语义 / 模型理论观点之间存在重要联系。我们将在此过程中探索其中的一些联系。例如，我们将看到，可以将“有效”断言视为在所有可能的非固定符号解释下都为真的断言，将“有效”推论视为在所有可能的状态和事务中都保持真实的推论。从这个角度来看，演绎系统应该只允许我们推导出有效的断言和蕴涵，这种属性称为健全性。如果演绎系统足够强大，可以让我们验证所有有效的断言和蕴涵，则称其为完备的。

There are important connections between the syntactic / deductive point of view on the one hand, and the semantic / model-theoretic point of view on the other. We will explore some of these along the way. For example, we will see that it is possible to view the “valid” assertions as those that are true under all possible interpretations of the non-fixed symbols, and the “valid” inferences as those that maintain truth in all possible states and affairs. From this point of view, a deductive system should only allow us to derive valid assertions and entailments, a property known as soundness. If a deductive system is strong enough to allow us to verify all valid assertions and entailments, it is said to be complete.

本课程的第四个目标是传达逻辑的语义观点，并引导您了解如何使用逻辑表达式来指定事态。

The fourth goal of this course is to convey the semantic view of logic, and to lead you to understand how logical expressions can be used to specify states of affairs.

1.5.目标总结¶

1.5. Goals Summarized¶

总而言之，本课程的目标是：

To summarize, these are the goals of this course:

• 您应该学会写出清晰的、“有文化的”数学证明。

• You should learn to write clear, “literate,” mathematical proofs.

• 您应该熟悉符号逻辑和演绎证明的形式建模。

• You should become comfortable with symbolic logic and the formal modeling of deductive proof.

• 您应该学习如何使用交互式校对助手。

• You should learn how to use an interactive proof assistant.

• 您应该了解如何使用逻辑作为一种精确的语言来对对象系统及其之间的关系提出主张，并指定某些事态。

• You should understand how to use logic as a precise language for making claims about systems of objects and the relationships between them, and specifying certain states of affairs.

让我们花点时间考虑一下这些目标之间的关系。重要的是不要混淆前三个目标。我们处理的是三种数学语言：普通数学语言、数学逻辑的符号表示和交互式证明助手中的计算实现。这些都是非常不同的东西！

Let us take a moment to consider the relationship between some of these goals. It is important not to confuse the first three. We are dealing with three kinds of mathematical language: ordinary mathematical language, the symbolic representations of mathematical logic, and computational implementations in interactive proof assistants. These are very different things!

符号逻辑并非旨在取代普通数学语言，你不应该使用如下符号$\wedge$和$\vee$在普通的数学证明中，符号表达式的作用并不比在写给父母的信中用符号表达式代替“and”和“or”要大。自然语言提供了表达的细微差别，可以传达超越模式匹配验证正确性的多层次含义和理解。同时，用符号表达式对数学语言进行建模提供了一定程度的精确度，使得将数学语言本身变成研究对象成为可能。每种表达式都有其适用之处，我们希望让您在不混淆两者的情况下欣赏每种表达式的价值。

Symbolic logic is not meant to replace ordinary mathematical language, and you should not use symbols like $\wedge$ and $\vee$ in ordinary mathematical proofs any more than you would use them in place of the words “and” and “or” in letters home to your parents. Natural languages provide nuances of expression that can convey levels of meaning and understanding that go beyond pattern matching to verify correctness. At the same time, modeling mathematical language with symbolic expressions provides a level of precision that makes it possible to turn mathematical language itself into an object of study. Each has its place, and we hope to get you to appreciate the value of each without confusing the two.

交互式定理证明器使用的证明语言介于两个极端之间。一方面，它们必须具有足够的精度，以便计算机能够处理它们并做出适当的反应；另一方面，它们旨在捕捉非正式语言的一些高级细微差别和特征，以便我们能够编写更复杂的论证和证明。它们植根于符号逻辑，并在设计时考虑到了普通数学语言，旨在弥合两者之间的差距。

The proof languages used by interactive theorem provers lie somewhere between the two extremes. On the one hand, they have to be specified with enough precision for a computer to process them and act appropriately; on the other hand, they aim to capture some of the higher-level nuances and features of informal language in a way that enables us to write more complex arguments and proofs. Rooted in symbolic logic and designed with ordinary mathematical language in mind, they aim to bridge the gap between the two.

本书还旨在向您展示数学是如何从基本概念构建起来的。逻辑提供了游戏规则，然后我们从集合、关系、函数和自然数的性质逐步发展到初等数论、组合学和实数的性质。最后一章以对公理基础的讨论结束了这个故事。

This book also aims to show you how mathematics is built up from fundamental concepts. Logic provides the rules of the game, and then we work our way up from properties of sets, relations, functions, and the natural numbers to elementary number theory, combinatorics, and properties of the real numbers. The last chapter rounds out the story with a discussion of axiomatic foundations.

1.6.关于本教材¶

1.6. About this Textbook¶

这本在线教科书和Lean定理证明器都是新项目，正在进行中。您可以从其项目页面、Leann社区页面和在线教科书《Lean 中的定理证明》了解有关 Lean 的更多信息。

Both this online textbook and the Lean theorem prover are new and ongoing projects. You can learn more about Lean from its project page, the Leann community pages, and the online textbook, Theorem Proving in Lean.

我们非常感谢许多人的反馈和更正，包括 Bruno Cuconato、William DeMeo、Tobias Grosser、Lyle Kopnicky、Alexandre Rademaker、Matt Rice 和 Jason Siefken。

We are grateful for feedback and corrections from a number of people, including Bruno Cuconato, William DeMeo, Tobias Grosser, Lyle Kopnicky, Alexandre Rademaker, Matt Rice, and Jason Siefken.

2.1.谜题¶

2.1. A Puzzle¶

下面的谜题名为“恶意与爱丽丝”，出自乔治·J·萨默斯的《逻辑推理谜题》。

The following puzzle, titled “Malice and Alice,” is from George J. Summers’ Logical Deduction Puzzles.

爱丽丝、爱丽丝的丈夫、他们的儿子、他们的女儿以及爱丽丝的兄弟卷入了一起谋杀案。五人中的一人杀死了另外四人中的一人。以下事实涉及上述五个人：

Alice, Alice’s husband, their son, their daughter, and Alice’s brother were involved in a murder. One of the five killed one of the other four. The following facts refer to the five people mentioned:

1. 谋杀案发生时，一名男子和一名女子正一起在酒吧里。

2. A man and a woman were together in a bar at the time of the murder.

3. 案发时，受害者和凶手正一起在海滩上。

4. The victim and the killer were together on a beach at the time of the murder.

5. 谋杀案发生时，爱丽丝的两个孩子中有一个是独自一人。

6. One of Alice’s two children was alone at the time of the murder.

7. 谋杀案发生时，爱丽丝和她的丈夫并不在一起。

8. Alice and her husband were not together at the time of the murder.

9. 受害者的双胞胎姐妹并不是凶手。

10. The victim’s twin was not the killer.

11. 凶手比受害者年轻。

12. The killer was younger than the victim.

这五个人中哪一个是受害者？

Which one of the five was the victim?

花点时间尝试找出解决方案。（你应该假设受害者的双胞胎是上述五个人之一。）萨默斯的书提供了以下提示：“首先找到谋杀案发生时两对人的位置，然后确定凶手和受害者是谁，这样就不会出现矛盾的情况。”

Take some time to try to work out a solution. (You should assume that the victim’s twin is one of the five people mentioned.) Summers’ book offers the following hint: “First find the locations of two pairs of people at the time of the murder, and then determine who the killer and the victim were so that no condition is contradicted.”

2.2.解决方案¶

2.2. A Solution¶

如果您曾经解答过这个谜题，那么您可能已经注意到一些事情。首先，绘制图表并系统地寻找答案是有帮助的。角色、位置和属性的数量是有限的，因此需要考虑的可能“事态”只有有限个。这些数字也足够小，因此系统地搜索所有可能性虽然很乏味，但最终会让您找到正确答案。这是这类逻辑谜题的一个特殊功能；例如，您不会期望通过遍历所有可能性来证明每个大于 2 的偶数都可以写成素数之和。

If you have worked on the puzzle, you may have noticed a few things. First, it is helpful to draw a diagram, and to be systematic about searching for an answer. The number of characters, locations, and attributes is finite, so that there are only finitely many possible “states of affairs” that need to be considered. The numbers are also small enough so that systematic search through all the possibilities, though tedious, will eventually get you to the right answer. This is a special feature of logic puzzles like this; you would not expect to show, for example, that every even number greater than two can be written as a sum of primes by running through all the possibilities.

您可能还注意到，这个问题似乎预设了这个问题有一个唯一的答案，也就是说，在所有符合条件的情况中，只有一个人可能是凶手。先验地，如果没有这个假设，找到某个可能是受害者的人和证明这个人一定是受害者之间是有区别的。换句话说，展示符合条件的情况和最终证明没有其他解决方案之间是有区别的。

Another thing that you may have noticed is that the question seems to presuppose that there is a unique answer to the question, which is to say, over all the states of affairs that meet the list of conditions, there is only one person who can possibly be the killer. A priori, without that assumption, there is a difference between finding some person who could have been the victim and showing that that person had to be the victim. In other words, there is a difference between exhibiting some state of affairs that meets the criteria and demonstrating conclusively that no other solution is possible.

书中公布的解决方案不仅产生了符合标准的情况，而且同时证明了这是唯一符合标准的情况。全文引述如下。

The published solution in the book not only produces a state of affairs that meets the criterion, but at the same time proves that this is the only one that does so. It is quoted below, in full.

从（1）、（2）、（3）中，五个人的角色分别是：酒吧里的男人和女人，海滩上的杀手和受害者，以及单独的孩子。

From (1), (2), and (3), the roles of the five people were as follows: Man and Woman in the bar, Killer and Victim on the beach, and Child alone.

然后，从 (4) 来看，要么爱丽丝的丈夫在酒吧而爱丽丝在海滩上，要么爱丽丝在酒吧而爱丽丝的丈夫在海滩上。

Then, from (4), either Alice’s husband was in the bar and Alice was on the beach, or Alice was in the bar and Alice’s husband was on the beach.

如果爱丽丝的丈夫在酒吧里，和他在一起的女人是他的女儿，独自一人的孩子是他的儿子，而爱丽丝和她的兄弟在海滩上。那么爱丽丝或她的兄弟就是受害者；所以另一个就是凶手。但是，从（5）来看，受害者有一个双胞胎，而这个双胞胎是无辜的。由于爱丽丝和她的兄弟只能是彼此的双胞胎，这种情况是不可能的。因此爱丽丝的丈夫不在酒吧里。

If Alice’s husband was in the bar, the woman he was with was his daughter, the child who was alone was his son, and Alice and her brother were on the beach. Then either Alice or her brother was the victim; so the other was the killer. But, from (5), the victim had a twin, and this twin was innocent. Since Alice and her brother could only be twins to each other, this situation is impossible. Therefore Alice’s husband was not in the bar.

所以 Alice 在酒吧里。如果 Alice 在酒吧里，那她一定是和她的兄弟或儿子在一起的。

So Alice was in the bar. If Alice was in the bar, she was with her brother or her son.

如果爱丽丝和她哥哥在一起，那么她的丈夫就会带着两个孩子中的一个在海滩上。从（5）来看，受害者不可能是她的丈夫，因为其他人都不可能是他的双胞胎；所以凶手是她的丈夫，受害者是他身边的孩子。但这种情况是不可能的，因为它与（6）相矛盾。因此，爱丽丝没有和她的哥哥一起在酒吧里。

If Alice was with her brother, her husband was on the beach with one of the two children. From (5), the victim could not be her husband, because none of the others could be his twin; so the killer was her husband and the victim was the child he was with. But this situation is impossible, because it contradicts (6). Therefore, Alice was not with her brother in the bar.

所以爱丽丝和她的儿子在酒吧里。那么那个独自一人的孩子就是她的女儿。因此，爱丽丝的丈夫和爱丽丝的兄弟一起在海滩上。从之前的推理来看，受害者不可能是爱丽丝的丈夫。但受害者可能是爱丽丝的兄弟，因为爱丽丝可能是他的双胞胎。

So Alice was with her son in the bar. Then the child who was alone was her daughter. Therefore, Alice’s husband was with Alice’s brother on the beach. From previous reasoning, the victim could not be Alice’s husband. But the victim could be Alice’s brother because Alice could be his twin.

所以爱丽丝的兄弟是受害者，而爱丽丝的丈夫是凶手。

So Alice’s brother was the victim and Alice’s husband was the killer.

这一论证依赖于一些“逻辑之外”的因素，例如，父亲不可能比孩子年轻，父母和孩子不可能是双胞胎。但这一论证还涉及许多常见的逻辑术语和相关的推理模式。在下一节中，我们将重点讨论上述论证中出现的一些关键逻辑术语，如“和”、“或”、“不”和“如果……那么”等词。

This argument relies on some “extralogical” elements, for example, that a father cannot be younger than his child, and that a parent and his or her child cannot be twins. But the argument also involves a number of common logical terms and associated patterns of inference. In the next section, we will focus on some of the key logical terms occurring in the argument above, words like “and,” “or,” “not,” and “if … then.”

我们的目标是解释控制这些术语使用的推理模式。为此，我们将使用符号逻辑的方法引入变量$A$，$B$，$C$，…代表基本陈述或命题和符号$\wedge$，$\vee$，$\mathrm{\neg }$， 和$\to$分别代表“和”、“或”、“非”和“如果……那么……”。这样做可以让我们专注于复合语句是如何利用逻辑术语从基本语句构建而成的，同时抽象出具体的内容。我们还将采用一种程式化的符号来表示推理规则：铭文

Our goal is to give an account of the patterns of inference that govern the use of those terms. To that end, using the methods of symbolic logic, we will introduce variables $A$, $B$, $C$, … to stand for fundamental statements, or propositions, and symbols $\wedge$, $\vee$, $\mathrm{\neg }$, and $\to$ to stand for “and,” “or,” “not,” and “if … then … ,” respectively. Doing so will let us focus on the way that compound statements are built up from basic ones using the logical terms, while abstracting away from the specific content. We will also adopt a stylized notation for representing inferences as rules: the inscription

表示该语句$C$是合乎逻辑的结果$A$和$B$。

indicates that statement $C$ is a logical consequence of $A$ and $B$.

2.3.推理规则¶

2.3. Rules of Inference¶

2.3.1.含义¶

2.3.1. Implication¶

我们将要讨论的第一个推理模式涉及“如果……那么……”结构，可能很难辨别。它的使用在很大程度上隐含在上述解决方案中。第四段中的推理更详细地阐述如下：

The first pattern of inference we will discuss, involving the “if … then …” construct, can be hard to discern. Its use is largely implicit in the solution above. The inference in the fourth paragraph, spelled out in greater detail, runs as follows:

---

如果爱丽丝在酒吧，那么爱丽丝就和她的兄弟或儿子在一起。

If Alice was in the bar, Alice was with her brother or her son.

爱丽丝在酒吧里。

Alice was in the bar.

爱丽丝和她的兄弟或儿子在一起。

Alice was with her brother or son.

---

这条规则有时被称为肯定前件法，即“蕴涵消除法”，因为它告诉我们如何在论证中使用蕴涵。一般来说，它表达如下：

This rule is sometimes known as modus ponens, or “implication elimination,” since it tells us how to use an implication in an argument. As a rule, it is expressed as follows:

读这句话的意思是，如果你有证据$A\to B$，可能来自一些假设，以及$A$，可能来自假设，然后结合这些假设得出$B$，来自两个子证明中的假设。

Read this as saying that if you have a proof of $A\to B$, possibly from some hypotheses, and a proof of $A$, possibly from hypotheses, then combining these yields a proof of $B$, from the hypotheses in both subproofs.

推导“如果……那么”陈述的规则更加微妙。考虑第三段的开头，其中论证了如果爱丽丝的丈夫在酒吧，那么爱丽丝或她的兄弟就是受害者。抽象出一些细节，该论点具有以下形式：

The rule for deriving an “if … then” statement is more subtle. Consider the beginning of the third paragraph, which argues that if Alice’s husband was in the bar, then Alice or her brother was the victim. Abstracting away some of the details, the argument has the following form:

---

假设爱丽丝的丈夫在酒吧。

Suppose Alice’s husband was in the bar.

然后 …

Then …

然后 …

Then …

那么爱丽丝或她的兄弟就是受害者。

Then Alice or her brother was the victim.

因此，如果爱丽丝的丈夫在酒吧，那么爱丽丝或她的兄弟就是受害者。

Thus, if Alice’s husband was in the bar, then Alice or her brother was the victim.

---

这是一种假设推理。假设$A$成立，我们认为$B$也成立。如果我们成功了，我们已经证明了$A$暗示$B$，不假设$A$换句话说，暂时假设$A$通过在结论中明确说明，成立被“取消”。

This is a form of hypothetical reasoning. On the supposition that $A$ holds, we argue that $B$ holds as well. If we are successful, we have shown that $A$ implies $B$, without supposing $A$. In other words, the temporary assumption that $A$ holds is “canceled” by making it explicit in the conclusion.

假设被贴上标签$1$；当应用引入规则时，标签$1$表示相关假设。假设上方的线表示该假设已被引入规则“取消”。

The hypothesis is given the label $1$; when the introduction rule is applied, the label $1$ indicates the relevant hypothesis. The line over the hypothesis indicates that the assumption has been “canceled” by the introduction rule.

2.3.2.连词¶

2.3.2. Conjunction¶

和蕴涵一样，其他逻辑联结词通常以引入和消除规则为特征。引入规则显示如何建立涉及联结词的断言，而消除规则显示如何使用包含联结词的断言导出其他断言。

As was the case for implication, other logical connectives are generally characterized by their introduction and elimination rules. An introduction rule shows how to establish a claim involving the connective, while an elimination rule shows how to use such a statement that contains the connective to derive others.

例如，让我们考虑一下连词的情况，即单词“and”。非正式地，我们通过建立每个连词来建立连词。例如，非正式地，我们可以论证：

Let us consider, for example, the case of conjunction, that is, the word “and.” Informally, we establish a conjunction by establishing each conjunct. For example, informally we might argue:

---

受害者是爱丽丝的哥哥。

Alice’s brother was the victim.

爱丽丝的丈夫就是凶手。

Alice’s husband was the killer.

因此，爱丽丝的兄弟是受害者，而爱丽丝的丈夫是凶手。

Therefore Alice’s brother was the victim and Alice’s husband was the killer.

---

这个推论似乎太明显了，无法明确说明，因为“和”这个词只是将两个断言合并为一个。非正式证明通常会淡化这种区别。在符号逻辑中，规则如下：

The inference seems almost too obvious to state explicitly, since the word “and” simply combines the two assertions into one. Informal proofs often downplay the distinction. In symbolic logic, the rule reads as follows:

通过两个消除规则，我们可以提取两个组成部分：

The two elimination rules allow us to extract the two components:

---

爱丽丝的丈夫在酒吧，而爱丽丝则在海滩上。

Alice’s husband was in the bar and Alice was on the beach.

原来爱丽丝的丈夫在酒吧里。

So Alice’s husband was in the bar.

---

或者：

Or:

---

爱丽丝的丈夫在酒吧，而爱丽丝则在海滩上。

Alice’s husband was in the bar and Alice was on the beach.

所以爱丽丝就在海滩上。

So Alice was on the beach.

---

在符号中，这些模式呈现如下：

In symbols, these patterns are rendered as follows:

这里$l$和$r$代表“左”和“右”。

Here the $l$ and $r$ stand for “left” and “right”.

2.3.3.否定与假¶

2.3.3. Negation and Falsity¶

从逻辑上讲，证明“非 A”就等于证明 A 会导致矛盾。例如：

In logical terms, showing “not A” amounts to showing that A leads to a contradiction. For example:

---

假设爱丽丝的丈夫在酒吧。

Suppose Alice’s husband was in the bar.

…

…

这种情况是不可能的。

This situation is impossible.

因此爱丽丝的丈夫不在酒吧。

Therefore Alice’s husband was not in the bar.

---

这是另一种假设推理形式，类似于建立“如果……那么”语句时使用的推理：我们暂时假设 A，表明这会导致矛盾，并得出结论“非 A”成立。用符号表示，规则如下：

This is another form of hypothetical reasoning, similar to that used in establishing an “if … then” statement: we temporarily assume A, show that leads to a contradiction, and conclude that “not A” holds. In symbols, the rule reads as follows:

消除规则与这些规则是对偶的。它表示如果我们同时拥有“A”和“非 A”，那么我们就有矛盾。这种模式在下面的非正式论证中得到了说明，它隐含在“Malice and Alice”解决方案的第四段中。

The elimination rule is dual to these. It expresses that if we have both “A” and “not A,” then we have a contradiction. This pattern is illustrated in the informal argument below, which is implicit in the fourth paragraph of the solution to “Malice and Alice.”

---

凶手是艾丽丝的丈夫，受害者是他怀里的孩子。

The killer was Alice’s husband and the victim was the child he was with.

因此凶手并不比受害者年轻。

So the killer was not younger than his victim.

但根据（6），凶手比受害者年轻。

But according to (6), the killer was younger than his victim.

这种情况是不可能的。

This situation is impossible.

---

在符号逻辑中，推理规则表示如下：

In symbolic logic, the rule of inference is expressed as follows:

还要注意，在符号框架中，我们引入了一个新符号，$\mathrm{\perp }$它对应于自然语言短语，如“这是一个矛盾”或“这是不可能的”。

Notice also that in the symbolic framework, we have introduced a new symbol, $\mathrm{\perp }$. It corresponds to natural language phrases like “this is a contradiction” or “this is impossible.”

有哪些规则$\mathrm{\perp }$? 在下一章我们将要介绍的证明系统中，没有引入规则；“假”就是假，除了从矛盾的假设中提取它之外，没有其他方法可以证明它。另一方面，该系统提供了一条规则，允许我们从矛盾中得出任何结论：

What are the rules governing $\mathrm{\perp }$? In the proof system we will introduce in the next chapter, there is no introduction rule; “false” is false, and there should be no way to prove it, other than extract it from contradictory hypotheses. On the other hand, the system provides a rule that allows us to conclude anything from a contradiction:

消除规则也有一个花哨的拉丁名，ex falso sequitur quodlibet，意思是“任何你想要的结果都源于虚假”。

The elimination rule also has the fancy Latin name, ex falso sequitur quodlibet, which means “anything you want follows from falsity.”

从自然语言的角度来看，这种消除规则很难激发，但尽管如此，它对于捕捉常见的推理模式还是必要的。理解它的一种方法是这样的。考虑以下语句：

This elimination rule is harder to motivate from a natural language perspective, but, nonetheless, it is needed to capture common patterns of inference. One way to understand it is this. Consider the following statement:

---

对于每个自然数$n$， 如果$n$为素数且大于 2，则$n$很奇怪。

For every natural number $n$, if $n$ is prime and greater than 2, then $n$ is odd.

---

我们想说这是一个正确的陈述。但如果它是真的，那么对于任何特定的数字来说，它都是正确的$n$. 服用$n=2$，我们有以下陈述：

We would like to say that this is a true statement. But if it is true, then it is true of any particular number $n$. Taking $n=2$, we have the statement:

---

如果 2 为质数且大于 2，则 2 为奇数。

If 2 is prime and greater than 2, then 2 is odd.

---

在这个条件语句中，前件和后件都是假的。我们承诺说这个语句是真的，这一事实表明我们应该能够以某种方式证明，语句 2 是奇数，这是由错误语句 2 是素数且大于 2 得出的。前件假也巧妙地概括了这种推理。

In this conditional statement, both the antecedent and succedent are false. The fact that we are committed to saying that this statement is true shows that we should be able to prove, one way or another, that the statement 2 is odd follows from the false statement that 2 is prime and greater than 2. The ex falso neatly encapsulates this sort of inference.

请注意，如果我们定义$\mathrm{\neg }A$是$A\to \mathrm{\perp }$，那么否定的引入和消除规则无非就是蕴涵的引入和消除。我们可以想到$\mathrm{\neg }A$生动地表达为“如果$A$是真的，那么猪就有翅膀”，其中“猪有翅膀”代表$\mathrm{\perp }$。

Notice that if we define $\mathrm{\neg }A$ to be $A\to \mathrm{\perp }$, then the rules for negation introduction and elimination are nothing more than implication introduction and elimination, respectively. We can think of $\mathrm{\neg }A$ expressed colorfully by saying “if $A$ is true, then pigs have wings,” where “pigs have wings” stands for $\mathrm{\perp }$.

引入了表示“假”的符号后，再引入表示“真”的符号才是公平的。与“假”相反，“真”没有消除规则，只有引入规则：

Having introduced a symbol for “false,” it is only fair to introduce a symbol for “true.” In contrast to “false,” “true” has no elimination rule, only an introduction rule:

简单来说，“真”就是真。

Put simply, “true” is true.

2.3.4.析取¶

2.3.4. Disjunction¶

析取（也称为“或”）的引入规则很简单。例如，在提出的解决方案中，条件 (3) 得到满足的说法可以证明如下：

The introduction rules for disjunction, otherwise known as “or,” are straightforward. For example, the claim that condition (3) is met in the proposed solution can be justified as follows:

---

谋杀案发生时，爱丽丝的女儿独自一人。

Alice’s daughter was alone at the time of the murder.

因此，要么爱丽丝的女儿在谋杀案发生时独自一人，要么爱丽丝的儿子在谋杀案发生时独自一人。

Therefore, either Alice’s daughter was alone at the time of the murder, or Alice’s son was alone at the time of the murder.

---

从象征意义上来说，这两条引入规则如下：

In symbolic terms, the two introduction rules are as follows:

在这里，再次$l$和$r$代表“左”和“右”。

Here, again, the $l$ and $r$ stand for “left” and “right”.

析取消元法规则比较复杂，但它代表了一种基于案例的假设推理的自然形式。在“恶意和爱丽丝”的解决方案中出现的情况都是此规则的特殊情况，因此，构造一个新的例子来说明普遍现象将很有帮助。假设，在上面的论证中，我们已经确定爱丽丝的兄弟或儿子在酒吧，并且我们想为她的丈夫在海滩上的结论辩护。一种选择是通过案例进行辩论：首先，考虑她兄弟在酒吧的情况，并根据该假设为结论辩护；然后考虑她儿子在酒吧的情况，并根据第二个假设为同一结论辩护。由于这两个案例是详尽无遗的，如果我们知道结论在每种情况下都成立，我们就知道它完全成立。模式看起来像这样：

The disjunction elimination rule is trickier, but it represents a natural form of case-based hypothetical reasoning. The instances that occur in the solution to “Malice and Alice” are all special cases of this rule, so it will be helpful to make up a new example to illustrate the general phenomenon. Suppose, in the argument above, we had established that either Alice’s brother or her son was in the bar, and we wanted to argue for the conclusion that her husband was on the beach. One option is to argue by cases: first, consider the case that her brother was in the bar, and argue for the conclusion on the basis of that assumption; then consider the case that her son was in the bar, and argue for the same conclusion, this time on the basis of the second assumption. Since the two cases are exhaustive, if we know that the conclusion holds in each case, we know that it holds outright. The pattern looks something like this:

---

要么是爱丽丝的兄弟在酒吧里，要么是爱丽丝的儿子在酒吧里。

Either Alice’s brother was in the bar, or Alice’s son was in the bar.

假设，在第一种情况下，她的兄弟在酒吧。那么... 因此，她的丈夫在海滩上。

Suppose, in the first case, that her brother was in the bar. Then … Therefore, her husband was on the beach.

另一方面，假设她的儿子在酒吧。在这种情况下，…因此，在这种情况下，她的丈夫也在海滩上。

On the other hand, suppose her son was in the bar. In that case, … Therefore, in this case also, her husband was on the beach.

无论如何，我们已经确定她的丈夫当时在海滩上。

Either way, we have established that her husband was on the beach.

---

在符号中，此模式表达如下：

In symbols, this pattern is expressed as follows:

这种模式令人困惑的地方在于，它需要两个嵌套的假设推理实例：在第一个括号中，我们暂时假设$A$，在第二个区块中，我们暂时假设$B$尘埃落定后，我们已确立$C$彻底地。

What makes this pattern confusing is that it requires two instances of nested hypothetical reasoning: in the first block of parentheses, we temporarily assume $A$, and in the second block, we temporarily assume $B$. When the dust settles, we have established $C$ outright.

还有另一种通常与“或”一起使用的推理模式，如下例所示：

There is another pattern of reasoning that is commonly used with “or,” as in the following example:

---

要么是爱丽丝的丈夫在酒吧，要么是爱丽丝在酒吧。

Either Alice’s husband was in the bar, or Alice was in the bar.

爱丽丝的丈夫不在酒吧。

Alice’s husband was not in the bar.

所以爱丽丝在酒吧里。

So Alice was in the bar.

---

用符号表示的话，我们将此规则表达如下：

In symbols, we would render this rule as follows:

下一章我们将看到，可以从其他规则中推导出这条规则。因此，我们不会将其作为我们系统中的基本推理规则。

We will see in the next chapter that it is possible to derive this rule from the others. As a result, we will not take this to be a fundamental rule of inference in our system.

2.3.5.当且仅当¶

2.3.5. If and only if¶

在数学论证中，通常会说两个陈述，$A$和$B$， 那 ”$A$当且仅当$B$成立。”这个断言有时缩写为“$A$当且仅当$B$”，意思是$A$暗示$B$和$B$暗示$A$。我们没有必要在我们的逻辑语言中引入一个新的符号来模拟这个连接词，因为这个陈述可以像我们刚才所做的那样，用“暗示”和“和”来表达。但请注意，表达式的长度加倍了，因为$A$和$B$每一个都是重复的。因此，逻辑缩写既方便又自然。

In mathematical arguments, it is common to say of two statements, $A$ and $B$, that “$A$ holds if and only if $B$ holds.” This assertion is sometimes abbreviated “$A$ iff $B$,” and means simply that $A$ implies $B$ and $B$ implies $A$. It is not essential that we introduce a new symbol into our logical language to model this connective, since the statement can be expressed, as we just did, in terms of “implies” and “and.” But notice that the length of the expression doubles because $A$ and $B$ are each repeated. The logical abbreviation is therefore convenient, as well as natural.

“恶意与爱丽丝”的条件意味着爱丽丝在酒吧当且仅当爱丽丝的丈夫在海滩上。通过依次论证每个蕴涵，可以建立这样的陈述：

The conditions of “Malice and Alice” imply that Alice is in the bar if and only if Alice’s husband is on the beach. Such a statement is established by arguing for each implication in turn:

---

我声称爱丽丝在酒吧当且仅当爱丽丝的丈夫在海滩上。

I claim that Alice is in the bar if and only if Alice’s husband is on the beach.

为了理解这一点，首先假设爱丽丝在酒吧里。

To see this, first suppose that Alice is in the bar.

然后 …

Then …

因此爱丽丝的丈夫就在海滩上。

Hence Alice’s husband is on the beach.

相反，假设爱丽丝的丈夫在海滩上。

Conversely, suppose Alice’s husband is on the beach.

然后 …

Then …

因此爱丽丝就在酒吧里。

Hence Alice is in the bar.

---

请注意，在这个例子中，我们改变了陈述的形式，首先陈述结论，而不是在论证结束时陈述。这种“指示”在非正式论证中很常见，因为它有助于引导读者的期望并预示论证的发展方向。正式的演绎系统通常不会模拟这种细微差别，这一事实标志着正式论证和非正式论证之间的差异，我们将在下文中讨论这个话题。

Notice that with this example, we have varied the form of presentation, stating the conclusion first, rather than at the end of the argument. This kind of “signposting” is common in informal arguments, in that is helps guide the reader’s expectations and foreshadow where the argument is going. The fact that formal systems of deduction do not generally model such nuances marks a difference between formal and informal arguments, a topic we will return to below.

引言以自然演绎建模如下：

The introduction is modeled in natural deduction as follows:

iff 的消元规则并不复杂。用非正式的语言来说，这是“左”规则：

The elimination rules for iff are unexciting. In informal language, here is the “left” rule:

---

当且仅当爱丽丝的丈夫在海滩上时，爱丽丝才会在酒吧里。

Alice is in the bar if and only if Alice’s husband is on the beach.

爱丽丝在酒吧里。

Alice is in the bar.

因此，爱丽丝的丈夫就在海滩上。

Hence, Alice’s husband is on the beach.

---

而“正确”的规则恰恰相反。

The “right” rule simply runs in the opposite direction.

---

当且仅当爱丽丝的丈夫在海滩上时，爱丽丝才会在酒吧里。

Alice is in the bar if and only if Alice’s husband is on the beach.

爱丽丝的丈夫在海滩上。

Alice’s husband is on the beach.

因此，爱丽丝在酒吧里。

Hence, Alice is in the bar.

---

根据自然演绎推理，规则如下：

Rendered in natural deduction, the rules are as follows:

2.3.6.矛盾证明¶

2.3.6. Proof by Contradiction¶

我们看到了一个非正式论证的例子，它隐式地使用了否定的引入规则：

We saw an example of an informal argument that implicitly uses the introduction rule for negation:

---

假设爱丽丝的丈夫在酒吧。

Suppose Alice’s husband was in the bar.

…

…

这种情况是不可能的。

This situation is impossible.

因此爱丽丝的丈夫不在酒吧。

Therefore Alice’s husband was not in the bar.

---

考虑以下论点：

Consider the following argument:

---

假设爱丽丝的丈夫不在海滩上。

Suppose Alice’s husband was not on the beach.

…

…

这种情况是不可能的。

This situation is impossible.

因此爱丽丝的丈夫就在海滩上。

Therefore Alice’s husband was on the beach.

---

乍一看，你可能会认为这个论证遵循与前一个论证相同的模式。但仔细观察就会发现一个区别：在第一个论证中，结论中引入了一个否定，而在第二个论证中，否定从假设中被消除。使用否定引入来结束第二个论证将得出结论“爱丽丝的丈夫不在海滩上的情况并非如此。”用肯定的陈述“爱丽丝的丈夫在海滩上”取代结论的推理规则称为矛盾证明。（它还有一个花哨的名字，即“归谬法”，即“归谬法”）。

At first glance, you might think this argument follows the same pattern as the one before. But a closer look should reveal a difference: in the first argument, a negation is introduced into the conclusion, whereas in the second, it is eliminated from the hypothesis. Using negation introduction to close the second argument would yield the conclusion “It is not the case that Alice’s husband was not on the beach.” The rule of inference that replaces the conclusion with the positive statement that Alice’s husband was on the beach is called a proof by contradiction. (It also has a fancy name, reductio ad absurdum, “reduction to an absurdity.”)

可能很难看出这两条规则之间的区别，因为我们通常认为“爱丽丝的丈夫不在海滩上”这句话是爱丽丝的丈夫在海滩上的拐弯抹角和近乎不合语法的说法。事实上，这条规则相当于增加了一条公理，即对于每个语句 A，“不不是 A”等同于 A。

It may be hard to see the difference between the two rules, because we commonly take the statement “Alice’s husband was not not on the beach” to be a roundabout and borderline ungrammatical way of saying that Alice’s husband was on the beach. Indeed, the rule is equivalent to adding an axiom that says that for every statement A, “not not A” is equivalent to A.

有一种数学方法被称为“构造性数学”，它否定“非非 A”与 A 的等价性。构造性论证往往具有更好的计算解释；某事为真的证明应该提供明确的证据证明该陈述为真，而不是提供该陈述不可能为假的证据。我们将在后面的章节中讨论构造性推理。尽管如此，矛盾证明在当代数学中被广泛使用，因此，在此期间，我们将自由使用矛盾证明作为我们的基本规则之一。

There is a style of doing mathematics known as “constructive mathematics” that denies the equivalence of “not not A” and A. Constructive arguments tend to have much better computational interpretations; a proof that something is true should provide explicit evidence that the statement is true, rather than evidence that it can’t possibly be false. We will discuss constructive reasoning in a later chapter. Nonetheless, proof by contradiction is used extensively in contemporary mathematics, and so, in the meanwhile, we will use proof by contradiction freely as one of our basic rules.

在自然演绎中，矛盾证明用以下模式表达：

In natural deduction, proof by contradiction is expressed by the following pattern:

假设$\mathrm{\neg }A$在最终推理时被取消。

The assumption $\mathrm{\neg }A$ is canceled at the final inference.

2.4.命题逻辑的语言¶

2.4. The Language of Propositional Logic¶

命题逻辑的语言始于符号$A$，$B$，$C$，……旨在涵盖基本断言或命题，这些断言或命题可以是真或假。复合表达式由括号和上一节介绍的逻辑符号组成。例如，

The language of propositional logic starts with symbols $A$, $B$, $C$, … which are intended to range over basic assertions, or propositions, which can be true or false. Compound expressions are built up using parentheses and the logical symbols introduced in the last section. For example,

是命题公式的一个例子。

is an example of a propositional formula.

在用符号逻辑编写表达式时，我们将采用一种运算顺序，这样我们就可以删除多余的括号。解析表达式时：

When writing expressions in symbolic logic, we will adopt an order of operations which allows us to drop superfluous parentheses. When parsing an expression:

• 否定的结合最为紧密。

• Negation binds most tightly.

• 然后，连词和析取词从右到左绑定。

• Then, conjunctions and disjunctions bind from right to left.

• 最后，蕴涵和双重蕴涵从右到左绑定。

• Finally, implications and bi-implications bind from right to left.

例如，表达式$\mathrm{\neg }A\vee B\to C\wedge D$被理解为$((\mathrm{\neg }A)\vee B)\to (C\wedge D)$。

So, for example, the expression $\mathrm{\neg }A\vee B\to C\wedge D$ is understood as $((\mathrm{\neg }A)\vee B)\to (C\wedge D)$.

例如，假设我们分配以下变量：

For example, suppose we assign the following variables:

• $A$：爱丽丝的丈夫在酒吧里

• $A$: Alice’s husband was in the bar

• $B$：爱丽丝在海滩上

• $B$: Alice was on the beach

• $C$：爱丽丝在酒吧里

• $C$: Alice was in the bar

• $D$：爱丽丝的丈夫在海滩上

• $D$: Alice’s husband was on the beach

那么“要么爱丽丝的丈夫在酒吧，爱丽丝在海滩上，或者爱丽丝在酒吧，爱丽丝的丈夫在海滩上”这句话将被表达为

Then the statement “either Alice’s husband was in the bar and Alice was on the beach, or Alice was in the bar and Alice’s husband was on the beach” would be rendered as

然而，有时合适的翻译并不那么简单。由于自然语言更加灵活和细致入微，因此需要一定程度的抽象和规范来进行翻译。有时不同的翻译可以说是合理的。在令人满意的情况下，替代翻译在逻辑上是等价的，即人们可以使用纯逻辑规则从另一个翻译中得出一个翻译。在不太令人满意的情况下，翻译将不等价，在这种情况下，从逻辑的角度来看，原始陈述只是模棱两可的。在这种情况下，选择符号表示有助于澄清预期的含义。

Sometimes the appropriate translation is not so straightforward, however. Because natural language is more flexible and nuanced, a degree of abstraction and regimentation is needed to carry out the translation. Sometimes different translations are arguably reasonable. In happy situations, alternative translations will be logically equivalent, in the sense that one can derive each from the other using purely logical rules. In less happy situations, the translations will not be equivalent, in which case the original statement is simply ambiguous, from a logical point of view. In cases like that, choosing a symbolic representation helps clarify the intended meaning.

例如，考虑这样一句话：“爱丽丝和她的儿子在海滩上，但她的丈夫独自一人。”我们可以选择以下变量：

Consider, for example, a statement like “Alice was with her son on the beach, but her husband was alone.” We might choose variables as follows:

• $A$：爱丽丝在海滩上

• $A$: Alice was on the beach

• $B$：爱丽丝的儿子在海滩上

• $B$: Alice’s son was on the beach

• $C$：爱丽丝的丈夫独自一人

• $C$: Alice’s husband was alone

在这种情况下，我们可以用符号表示语句为$A\wedge B\wedge C$。使用“with”一词似乎不仅仅意味着爱丽丝和她的儿子都在海滩上；例如，它似乎意味着他们意识到彼此的存在、互动等。同样，虽然我们已经翻译了“but”和“and”，但“but”一词也传达了信息；在这种情况下，它似乎强调了对比，而在其他情况下，它可以用来断言与预期相反的事实。因此，在这两种情况下，逻辑渲染都对原始句子的某些特征进行建模，同时抽象其他特征。

In that case, we might represent the statement in symbols as $A\wedge B\wedge C$. Using the word “with” may seem to connote more than the fact that Alice and her son were both on the beach; for example, it seems to connote that they aware of each others’ presence, interacting, etc. Similarly, although we have translated the word “but” and “and,” the word “but” also convey information; in this case, it seems to emphasize a contrast, while in other situations, it can be used to assert a fact that is contrary to expectations. In both cases, then, the logical rendering models certain features of the original sentence while abstracting others.

2.5.练习¶

2.5. Exercises¶

1. 这是乔治·J·萨默斯 (George J. Summers) 的另一个（可怕的）逻辑谜题，名为“家庭谋杀案”。

   一天晚上，一对父母和他们的儿子和女儿的家里发生了一起谋杀案。一名家庭成员谋杀了另一名家庭成员，第三名家庭成员目击了整个过程，第四名家庭成员则是事后共犯。

   1. 同案犯与证人性别相反。

   2. 最年长的成员与证人是异性。

   3. 最年轻的成员与受害者是异性。

   4. 该附属品的年龄比受害者的年龄还要大。

   5. 父亲是成员中年龄最大的。

   6. 凶手并不是最年轻的成员。

   父亲、母亲、儿子、女儿这四个人中，哪一个是凶手？

   解决这个难题，并写出一个清晰的论据来证明你的答案是正确的。

2. Here is another (gruesome) logic puzzle by George J. Summers, called “Murder in the Family.”

   Murder occurred one evening in the home of a father and mother and their son and daughter. One member of the family murdered another member, the third member witnessed the crime, and the fourth member was an accessory after the fact.

   1. The accessory and the witness were of opposite sex.

   2. The oldest member and the witness were of opposite sex.

   3. The youngest member and the victim were of opposite sex.

   4. The accessory was older than the victim.

   5. The father was the oldest member.

   6. The murderer was not the youngest member.

   Which of the four—father, mother, son, or daughter—was the murderer?

   Solve this puzzle, and write a clear argument to establish that your answer is correct.

3. 使用助记符$F$（父亲），$M$（母亲），$D$（女儿），$S$（儿子），$Mu$（凶手），$V$（受害者），$W$（证人），$A$（配饰），$O$（最老的），$Y$（最年轻），我们可以定义命题变量，如$FM$（父亲是凶手）$DV$（女儿是受害者）$FO$（父亲是长子），$VY$（受害者是最年轻的）等等。请注意，只有儿子或女儿可以是最小的，只有母亲或父亲可以是最年长的。

   按照这些约定，第一个线索可以表示为

   $$((FA\vee SA)\to (MW\vee DW))\wedge ((MA\vee DA)\to (FW\vee SW)),$$

   换句话说，如果父亲或儿子是从犯，那么母亲或女儿就是证人，反之亦然。以类似的方式表示其他五条线索。

   表示第四条线索比较棘手。尝试写下一个公式，描述信息未排除的所有可能性。

4. Using the mnemonic $F$ (Father), $M$ (Mother), $D$ (Daughter), $S$ (Son), $Mu$ (Murderer), $V$ (Victim), $W$ (Witness), $A$ (Accessory), $O$ (Oldest), $Y$ (Youngest), we can define propositional variables like $FM$ (Father is the Murderer), $DV$ (Daughter is the Victim), $FO$ (Father is Oldest), $VY$ (Victim is Youngest), etc. Notice that only the son or daughter can be the youngest, and only the mother or father can be the oldest.

   With these conventions, the first clue can be represented as

   $$((FA\vee SA)\to (MW\vee DW))\wedge ((MA\vee DA)\to (FW\vee SW)),$$

   in other words, if the father or son was the accessory, then the mother or daughter was the witness, and vice-versa. Represent the other five clues in a similar manner.

   Representing the fourth clue is tricky. Try to write down a formula that describes all the possibilities that are not ruled out by the information.

5. 考虑以下三个假设：

   • 艾伦喜欢袋鼠，而贝蒂喜欢青蛙，或者卡尔喜欢仓鼠。

   • 如果贝蒂喜欢青蛙，那么艾伦就不喜欢袋鼠。

   • 如果卡尔喜欢仓鼠，那么贝蒂就喜欢青蛙。

   写一个清晰的论据来表明这三个假设是矛盾的。

6. Consider the following three hypotheses:

   • Alan likes kangaroos, and either Betty likes frogs or Carl likes hamsters.

   • If Betty likes frogs, then Alan doesn’t like kangaroos.

   • If Carl likes hamsters, then Betty likes frogs.

   Write a clear argument to show that these three hypotheses are contradictory.

3.1.自然演绎中的推导¶

3.1. Derivations in Natural Deduction¶

我们已经看到，命题逻辑的语言允许我们从命题变量构建表达式$A,B,C,\dots$使用命题连接词，如$\to$，$\wedge$，$\vee$， 和$\mathrm{\neg }$。我们现在将考虑一个正式的演绎系统，我们可以用它来证明命题公式。有许多这样的系统可供选择；我们将使用的系统称为自然演绎，由 Gerhard Gentzen 在 20 世纪 30 年代设计。

We have seen that the language of propositional logic allows us to build up expressions from propositional variables $A,B,C,\dots$ using propositional connectives like $\to$, $\wedge$, $\vee$, and $\mathrm{\neg }$. We will now consider a formal deductive system that we can use to prove propositional formulas. There are a number of such systems on offer; the one will use is called natural deduction, designed by Gerhard Gentzen in the 1930s.

在自然演绎中，每个证明都是基于假设的证明。换句话说，在任何证明中，都有一组有限的假设$\{B,C,\dots \}$结论$A$，证明表明$A$遵循$B,C,\dots$。

In natural deduction, every proof is a proof from hypotheses. In other words, in any proof, there is a finite set of hypotheses $\{B,C,\dots \}$ and a conclusion $A$, and what the proof shows is that $A$ follows from $B,C,\dots$.

和公式一样，证明也是通过按照规则将较小的证明组合在一起而建立的。例如，阅读 and-introduction 规则的方法

Like formulas, proofs are built by putting together smaller proofs, according to the rules. For instance, the way to read the and-introduction rule

如下：如果你有证据$P_1$的$A$从一些假设中，你得到了一个证据$P_2$的$B$然后你可以用这个规则把它们放在一起，得到一个证明$A\wedge B$，它使用了$P_1$以及所有假设$P_2$。例如，这是$(A\wedge B)\wedge (A\wedge C)$从三个假设来看，$A$，$B$， 和$C$：

is as follows: if you have a proof $P_1$ of $A$ from some hypotheses, and you have a proof $P_2$ of $B$ from some hypotheses, then you can put them together using this rule to obtain a proof of $A\wedge B$, which uses all the hypotheses in $P_1$ together with all the hypotheses in $P_2$. For example, this is a proof of $(A\wedge B)\wedge (A\wedge C)$ from three hypotheses, $A$, $B$, and $C$:

在一些自然演绎的表示中，证明被写成一系列行，其中每一行都可以引用任何前面的行来证明。但在这里我们将采用严格的二维图解格式，其中每个推论的前提都出现在结论的正上方。这使得检查证明并检查其是否正确变得容易：每个推论都应该是用特定公式实例化规则之一中的字母的结果。

In some presentations of natural deduction, a proof is written as a sequence of lines in which each line can refer to any previous lines for justification. But here we will adopt a rigid two-dimensional diagrammatic format in which the premises of each inference appear immediately above the conclusion. This makes it easy to look over a proof and check that it is correct: each inference should be the result of instantiating the letters in one of the rules with particular formulas.

使自然演绎令人困惑的一件事是，当你以这种方式整理证明时，假设可以被消除，或者，正如我们所说的，被取消。例如，我们可以将隐含引入规则应用于最后一个证明，并得到以下证明$B\to (A\wedge B)\wedge (A\wedge C)$仅从两个假设来看，$A$和$C$：

One thing that makes natural deduction confusing is that when you put together proofs in this way, hypotheses can be eliminated, or, as we will say, canceled. For example, we can apply the implies-introduction rule to the last proof, and obtain the following proof of $B\to (A\wedge B)\wedge (A\wedge C)$ from only two hypotheses, $A$ and $C$:

这里，我们使用标签 1 来表示假设$B$已取消。任何标签都可以，但我们倾向于使用数字。

Here, we have used the label 1 to indicate the place where the hypothesis $B$ was canceled. Any label will do, though we will tend to use numbers for that purpose.

我们可以继续取消假设$A$：

We can continue to cancel the hypothesis $A$:

结果是仅使用假设的证明$C$我们也可以继续取消这个假设：

The result is a proof using only the hypothesis $C$. We can continue to cancel that hypothesis as well:

最终的证明根本不使用任何假设。换句话说，它直接确立了结论。

The resulting proof uses no hypothesis at all. In other words, it establishes the conclusion outright.

请注意，在第二步中，我们取消了假设的两个“副本”$A$。在自然演绎中，我们可以选择取消哪些假设；我们可以取消其中一个假设，而保留另一个假设。事实上，我们也可以执行蕴涵引入规则并取消零个假设。例如，以下是$A\to B$从假设$B$：

Notice that in the second step, we canceled two “copies” of the hypothesis $A$. In natural deduction, we can choose which hypotheses to cancel; we could have canceled either one, and left the other hypothesis open. In fact, we can also carry out the implication-introduction rule and cancel zero hypotheses. For example, the following is a short proof of $A\to B$ from the hypothesis $B$:

在这个证明中，$A$均被取消。

In this proof, zero copies of $A$ are canceled.

还请注意，尽管我们使用的字母$A$，$B$， 和$C$作为命题变量，在上面的证明中，我们可以用任何命题公式代替它们。例如，我们可以用$A$根据公式$(D\vee E)$处处，并且仍然有正确的证明。在某些逻辑表述中，命题变量和任意命题公式使用不同的字母，但我们将继续模糊区别。你可以认为$A$，$B$， 和$C$代表命题变量或公式，随你喜欢。如果你把它们看作命题变量，请记住，在任何规则或证明中，你可以用不同的公式替换每个变量，而仍然有有效的规则或证明。

Also notice that although we are using letters like $A$, $B$, and $C$ as propositional variables, in the proofs above we can replace them by any propositional formula. For example, we can replace $A$ by the formula $(D\vee E)$ everywhere, and still have correct proofs. In some presentations of logic, different letters are used for propositional variables and arbitrary propositional formulas, but we will continue to blur the distinction. You can think of $A$, $B$, and $C$ as standing for propositional variables or formulas, as you prefer. If you think of them as propositional variables, just keep in mind that in any rule or proof, you can replace every variable by a different formula, and still have a valid rule or proof.

最后，还要注意的是，在这些例子中，我们假设了一个特殊规则作为构建证明的起点。它被称为假设规则，它看起来像这样：

Finally, notice also that in these examples, we have assumed a special rule as the starting point for building proofs. It is called the assumption rule, and it looks like this:

这意味着在任何时候我们都可以自由地假设一个公式，$A$. 单一配方$A$构成一行证明，阅读此证明的方式如下：假设$A$，我们已经证明$A$。

What it means is that at any point we are free to simply assume a formula, $A$. The single formula $A$ constitutes a one-line proof, and the way to read this proof is as follows: assuming $A$, we have proved $A$.

其余的推理规则在上一章中给出，我们在此进行总结。

The remaining rules of inference were given in the last chapter, and we summarize them here.

含义：

Implication:

连词：

Conjunction:

否定：

Negation:

析取：

Disjunction:

真与假：

Truth and falsity:

双重含义：

Bi-implication:

归谬法（反证法）：

Reductio ad absurdum (proof by contradiction):

3.2.示例¶

3.2. Examples¶

让我们再考虑一些自然演绎证明的例子。在每种情况下，你都应该思考公式说了什么，以及每一步调用了哪条推理规则。还要密切注意每个阶段取消了哪些假设。如果你查看树的任何一个节点，那么在这一点上已经确定的是，该主张遵循它上面所有尚未取消的假设。

Let us consider some more examples of natural deduction proofs. In each case, you should think about what the formulas say and which rule of inference is invoked at each step. Also pay close attention to which hypotheses are canceled at each stage. If you look at any node of the tree, what has been established at that point is that the claim follows from all the hypotheses above it that haven’t been canceled yet.

以下是证明$A\to C$从$A\to B$和$B\to C$：

The following is a proof of $A\to C$ from $A\to B$ and $B\to C$:

直观地看，公式

Intuitively, the formula

“内化”了先前证明的结论。$\wedge$符号用于组合假设，并且$\to$符号用来表示右边是左边的结果。下面是该公式的证明：

“internalizes” the conclusion of the previous proof. The $\wedge$ symbol is used to combine hypotheses, and the $\to$ symbol is used to express that the right-hand side is a consequence of the left. Here is a proof of that formula:

下一个证明表明，如果结论$C$，得出$A$和$B$，那么就可以从它们的合取中得出。

The next proof shows that if a conclusion, $C$, follows from $A$ and $B$, then it follows from their conjunction.

下一个证明的结论可以解释为，如果其中一个不是$A$或者$B$为真，则它们都是假的。它说明了否定规则的用法。

The conclusion of the next proof can be interpreted as saying that if it is not the case that one of $A$ or $B$ is true, then they are both false. It illustrates the use of the rules for negation.

最后，接下来的两个例子说明了ex falso规则的用法。第一个是任意公式的推导$B$从$\mathrm{\neg }A$和$A$：

Finally, the next two examples illustrate the use of the ex falso rule. The first is a derivation of an arbitrary formula $B$ from $\mathrm{\neg }A$ and $A$:

第二项显示$B$遵循$A$和$\mathrm{\neg }A\vee B$：

The second shows that $B$ follows from $A$ and $\mathrm{\neg }A\vee B$:

在一些证明系统中，这些规则被视为系统的一部分。但是在我们的系统中我们不需要这样做：这两个例子表明这些规则可以从我们的其他规则中推导出来。

In some proof systems, these rules are taken to be part of the system. But we do not need to that with our system: these two examples show that the rules can be derived from our other rules.

3.3.正向和反向推理¶

3.3. Forward and Backward Reasoning¶

自然演绎应该代表我们在处理逻辑谜题时使用的推理和论证模式的理想化模型，例如，在上一章中。它们之间存在明显的区别：我们用符号和二维图表描述自然演绎证明，而我们的非正式论证则用文字和段落来写。值得反思一下该模型捕捉到了什么。自然演绎应该阐明我们逻辑论证的形式和结构，描述证明结论的适当方法，并解释我们使用的规则在何种意义上是有效的。

Natural deduction is supposed to represent an idealized model of the patterns of reasoning and argumentation we use, for example, when working with logic puzzles as in the last chapter. There are obvious differences: we describe natural deduction proofs with symbols and two-dimensional diagrams, whereas our informal arguments are written with words and paragraphs. It is worthwhile to reflect on what is captured by the model. Natural deduction is supposed to clarify the form and structure of our logical arguments, describe the appropriate means of justifying a conclusion, and explain the sense in which the rules we use are valid.

构建自然演绎证明可能会令人困惑，但思考它为什么令人困惑是有帮助的。例如，我们可以决定自然演绎不是逻辑推理的好模型。或者我们可能会得出结论，自然演绎的令人困惑的特征告诉我们一些关于普通论证的有趣之处。

Constructing natural deduction proofs can be confusing, but it is helpful to think about why it is confusing. We could, for example, decide that natural deduction is not a good model for logical reasoning. Or we might come to the conclusion that the features of natural deduction that make it confusing tell us something interesting about ordinary arguments.

在“官方”描述中，自然演绎证明是通过将较小的证明放在一起得到较大的证明来构建的。为了证明$A\wedge B\to B\wedge A$，我们从假设开始$A\wedge B$。然后我们分别构造以下两个证明：

In the “official” description, natural deduction proofs are constructed by putting smaller proofs together to obtain bigger ones. To prove $A\wedge B\to B\wedge A$, we start with the hypothesis $A\wedge B$. Then we construct, separately, the following two proofs:

然后我们利用这两个证明构造以下证明：

Then we use these two proofs to construct the following one:

最后，我们将隐含引入规则应用于该证明以取消假设并得到所需的结论：

Finally, we apply the implies-introduction rule to this proof to cancel the hypothesis and obtain the desired conclusion:

该过程与非正式争论中发生的过程类似，我们从一些假设开始，然后逐步得出结论。

The process is similar to what happens in an informal argument, where we start with some hypotheses, and work forward towards a conclusion.

假设苏珊很高并且约翰很高兴。

Suppose Susan is tall and John is happy.

那么，约翰尤其高兴。

Then, in particular, John is happy.

此外，苏珊很高。

Also, Susan is tall.

所以约翰很高兴，苏珊也长高了。

So John is happy and Susan is tall.

因此，我们表明，如果苏珊身高较高且约翰很高兴，那么约翰也会很高兴且苏珊身高较高。

Therefore we have shown that if Susan is tall and John is happy, then John is happy and Susan is tall.

然而，当我们阅读自然演绎证明时，我们经常会倒着读。首先，我们查看底部以查看要证明的内容。然后我们考虑用于证明它的规则，并查看规则要求的前提。然后我们查看如何证明这些主张，等等。同样，当我们构建自然演绎证明时，我们通常也会倒着读：我们从要证明的主张开始，将其放在底部，然后寻找要应用的规则。

However, when we read natural deduction proofs, we often read them backward. First, we look at the bottom to see what is being proved. Then we consider the rule that is used to prove it, and see what premises the rule demands. Then we look to see how those claims are proved, and so on. Similarly, when we construct a natural deduction proof, we typically work backward as well: we start with the claim we are trying to prove, put that at the bottom, and look for rules to apply.

有时这个过程会崩溃。假设我们只剩下一个目标，那就是一个命题变量，$A$。没有可以应用的引入规则，因此，除非$A$是一个假设，它必须来自一个消除规则。但这没有明确问题：也许$A$通过将消去规则应用于$A\wedge B$或将或消除规则应用于$C$和$C\to A$。此时，我们会考虑假设，并开始向前推进。例如，如果我们的假设$C$和$C\to A\wedge B$，然后我们将继续努力获得$A\wedge B$和$A$。

At times that process breaks down. Suppose we are left with a goal that is a single propositional variable, $A$. There are no introduction rules that can be applied, so, unless $A$ is a hypothesis, it has to come from an elimination rule. But that underspecifies the problem: perhaps the $A$ comes from applying the and-elimination rule to $A\wedge B$, or from applying the or-elimination rule to $C$ and $C\to A$. At that point, we look to the hypotheses, and start working forward. If, for example, our hypotheses are $C$ and $C\to A\wedge B$, we would then work forward to obtain $A\wedge B$ and $A$.

因此，存在一种用于证明自然演绎定理的一般启发式方法：

There is thus a general heuristic for proving theorems in natural deduction:

1. 首先从结论开始，使用引言规则。例如，如果你试图证明以下形式的陈述$A\to B$， 添加$A$你的假设列表，并尝试推导出$B$. 如果你试图证明以下形式的陈述$A\wedge B$，使用 and-introduction 规则将你的任务简化为证明$A$，然后证明$B$。

2. Start by working backward from the conclusion, using the introduction rules. For example, if you are trying to prove a statement of the form $A\to B$, add $A$ to your list of hypotheses and try to derive $B$. If you are trying to prove a statement of the form $A\wedge B$, use the and-introduction rule to reduce your task to proving $A$, and then proving $B$.

3. 当你在第一步中没有事情要做时，使用消除规则来继续前进。如果你有假设$A\to B$和$A$，运用肯定前件推导出$B$. 如果你有一个假设$A\vee B$，使用或消除法来拆分案例，考虑$A$在一个案例中$B$在另一个。

4. When you have run out things to do in the first step, use elimination rules to work forward. If you have hypotheses $A\to B$ and $A$, apply modus ponens to derive $B$. If you have a hypothesis $A\vee B$, use or-elimination to split on cases, considering $A$ in one case and $B$ in the other.

在第 5 章中，我们将向此列表添加另一个元素：如果其他方法都失败了，请尝试反证法。

In Chapter 5 we will add one more element to this list: if all else fails, try a proof by contradiction.

正向推理和逆向推理之间的矛盾也存在于数学和其他领域的非正式论证中。当我们证明一个定理时，我们通常会使用假设、假设、定义和背景知识进行正向推理。但我们也会牢记目标，这有助于我们理解前进的步骤。

The tension between forward and backward reasoning is found in informal arguments as well, in mathematics and elsewhere. When we prove a theorem, we typically reason forward, using assumptions, hypotheses, definitions, and background knowledge. But we also keep the goal in mind, and that helps us make sense of the forward steps.

当我们转向交互式定理证明时，我们会看到精益具有支持正向和反向推理的机制。这些机制在非正式论证风格和自然演绎模型之间架起了一座桥梁，从而更清楚地展示了正在发生的事情。

When we turn to interactive theorem proving, we will see that Lean has mechanisms to support both forward and backward reasoning. These form a bridge between informal styles of argumentation and the natural deduction model, and thereby provide a clearer picture of what is going on.

自然演绎证明的另一个令人困惑的特征是，每个假设都有一个范围，也就是说，在证明中只有某些点可以使用假设。当然，这也是非正式数学论证的一个特点。假设一个段落以“让$x$是小于 100 的任何数字”，认为$x$最多有五个质因数，并得出结论“因此我们证明了每个小于 100 的数字最多有五个因数。”参考“$x$”，并且小于 100 的假设仅在该段落的范围内有效。如果下一段以“现在假设$x$是大于 100 的任何数字”，那么当然，假设$x$小于 100 不再适用。

Another confusing feature of natural deduction proofs is that every hypothesis has a scope, which is to say, there are only certain points in the proof where an assumption is available for use. Of course, this is also a feature of informal mathematical arguments. Suppose a paragraph begins “Let $x$ be any number less than 100,” argues that $x$ has at most five prime factors, and concludes “thus we have shown that every number less than 100 has at most five factors.” The reference “$x$”, and the assumption that it is less than 100, is only active within the scope of the paragraph. If the next paragraph begins with the phrase “Now suppose $x$ is any number greater than 100,” then, of course, the assumption that $x$ is less than 100 no longer applies.

在自然演绎中，假设从被假定的点到被取消的点都是可用的。我们将看到，交互式定理证明语言也有确定参考和假设范围的机制，这些机制也揭示了非形式数学中的范围问题。

In natural deduction, a hypothesis is available from the point where it is assumed until the point where it is canceled. We will see that interactive theorem proving languages also have mechanisms to determine the scope of references and hypotheses, and that these, too, shed light on scoping issues in informal mathematics.

3.4.案例推理¶

3.4. Reasoning by Cases¶

消除析取的规则令人困惑，但我们可以通过一个例子来理解它。考虑以下非正式论证：

The rule for eliminating a disjunction is confusing, but we can make sense of it with an example. Consider the following informal argument:

乔治要么在家，要么在校园。

George is either at home or on campus.

如果他在家，他就在学习。

If he is at home, he is studying.

如果他在校园，他就和他的朋友在一起。

If he is on campus, he is with his friends.

因此，乔治要么在学习，要么和他的朋友在一起。

Therefore, George is either studying or with his friends.

让$A$是乔治在家的陈述，让$B$是乔治在校园的声明，让$C$是乔治正在研究的陈述，并设$D$是乔治和他的朋友在一起的陈述。那么上面的论证有以下模式：从$A\vee B$，$A\to C$， 和$B\to D$，总结$C\vee D$。在自然演绎中，我们无法一步就得出这个结论，但将其充实为适当的证明并不需要太多工作。非正式地，我们必须进行如下论证。

Let $A$ be the statement that George is at home, let $B$ be the statement that George is on campus, let $C$ be the statement that George is studying, and let $D$ be the statement the George is with his friends. Then the argument above has the following pattern: from $A\vee B$, $A\to C$, and $B\to D$, conclude $C\vee D$. In natural deduction, we cannot get away with drawing this conclusion in a single step, but it does not take too much work to flesh it out into a proper proof. Informally, we have to argue as follows.

乔治要么在家，要么在校园。

Georges is either at home or on campus.

情况 1：假设他在家。我们知道如果他在家，那么他就在学习。所以，在这种情况下，他正在学习。因此，在这种情况下，他要么在学习，要么在和朋友在一起。

案例 2：假设他在校园里。我们知道，如果他在校园里，那么他就和他的朋友在一起。所以，在这种情况下，他和他的朋友在一起。因此，在这种情况下，他要么在学习，要么和他的朋友在一起。

Case 1: Suppose he is at home. We know that if he is at home, then he is studying. So, in this case, he is studying. Therefore, in this case, he is either studying or with his friends.

Case 2: Suppose he is on campus. We know that if he is on campus, then he is with his friends. So, in this case, he is with his friends. Therefore, in this case, he is either studying or with his friends.

无论怎样，乔治要么在学习，要么和他的朋友在一起。

Either way, George is either studying or with his friends.

自然演绎证明如下：

The natural deduction proof looks as follows:

你应该思考这个证明的结构如何反映其上方的非正式的基于案例的论点。

You should think about how the structure of this proof reflects the informal case-based argument above it.

再举一个例子，这是$A\wedge (B\vee C)\to (A\wedge B)\vee (A\wedge C)$：

For another example, here is a proof of $A\wedge (B\vee C)\to (A\wedge B)\vee (A\wedge C)$:

3.5.一些逻辑身份¶

3.5. Some Logical Identities¶

两个命题公式，$A$和$B$，如果​$A\leftrightarrow B$是可证明的。逻辑等价类似于恒等式，例如$x+y=y+x$代数中经常出现的公式。具体来说，可以证明如果两个公式等价，那么可以在任何公式中用一个公式代替另一个公式，结果也将等价。（一些证明系统将此视为基本规则，交互式定理证明器可以适应它，但我们不会将其视为自然演绎的基本规则。）

Two propositional formulas, $A$ and $B$, are said to be logically equivalent if $A\leftrightarrow B$ is provable. Logical equivalences are similar to identities like $x+y=y+x$ that occur in algebra. In particular, one can show that if two formulas are equivalent, then one can substitute one for the other in any formula, and the results will also be equivalent. (Some proof systems take this to be a basic rule, and interactive theorem provers can accommodate it, but we will not take it to be a fundamental rule of natural deduction.)

作为参考，以下列表包含一些常用的命题等价关系以及一些值得注意的公式。想想为什么直观上这些公式应该是正确的。

For reference, the following list contains some commonly used propositional equivalences, along with some noteworthy formulas. Think about why, intuitively, these formulas should be true.

1. 交换性$\wedge$：$A\wedge B\leftrightarrow B\wedge A$

2. Commutativity of $\wedge$: $A\wedge B\leftrightarrow B\wedge A$

3. 交换性$\vee$：$A\vee B\leftrightarrow B\vee A$

4. Commutativity of $\vee$: $A\vee B\leftrightarrow B\vee A$

5. 结合性$\wedge$：$(A\wedge B)\wedge C\leftrightarrow A\wedge (B\wedge C)$

6. Associativity of $\wedge$: $(A\wedge B)\wedge C\leftrightarrow A\wedge (B\wedge C)$

7. 结合性$\vee$ $(A\vee B)\vee C\leftrightarrow A\vee (B\vee C)$

8. Associativity of $\vee$ $(A\vee B)\vee C\leftrightarrow A\vee (B\vee C)$

9. 分配性$\wedge$超过$\vee$：$A\wedge (B\vee C)\leftrightarrow (A\wedge B)\vee (A\wedge C)$

10. Distributivity of $\wedge$ over $\vee$: $A\wedge (B\vee C)\leftrightarrow (A\wedge B)\vee (A\wedge C)$

11. 分配性$\vee$超过$\wedge$：$A\vee (B\wedge C)\leftrightarrow (A\vee B)\wedge (A\vee C)$

12. Distributivity of $\vee$ over $\wedge$: $A\vee (B\wedge C)\leftrightarrow (A\vee B)\wedge (A\vee C)$

13. $(A\to (B\to C))\leftrightarrow (A\wedge B\to C)$。

14. $(A\to (B\to C))\leftrightarrow (A\wedge B\to C)$.

15. $(A\to B)\to ((B\to C)\to (A\to C))$

16. $(A\to B)\to ((B\to C)\to (A\to C))$

17. $((A\vee B)\to C)\leftrightarrow (A\to C)\wedge (B\to C)$

18. $((A\vee B)\to C)\leftrightarrow (A\to C)\wedge (B\to C)$

19. $\mathrm{\neg }(A\vee B)\leftrightarrow \mathrm{\neg }A\wedge \mathrm{\neg }B$

20. $\mathrm{\neg }(A\vee B)\leftrightarrow \mathrm{\neg }A\wedge \mathrm{\neg }B$

21. $\mathrm{\neg }(A\wedge B)\leftrightarrow \mathrm{\neg }A\vee \mathrm{\neg }B$

22. $\mathrm{\neg }(A\wedge B)\leftrightarrow \mathrm{\neg }A\vee \mathrm{\neg }B$

23. $\mathrm{\neg }(A\wedge \mathrm{\neg }A)$

24. $\mathrm{\neg }(A\wedge \mathrm{\neg }A)$

25. $\mathrm{\neg }(A\to B)\leftrightarrow A\wedge \mathrm{\neg }B$

26. $\mathrm{\neg }(A\to B)\leftrightarrow A\wedge \mathrm{\neg }B$

27. $\mathrm{\neg }A\to (A\to B)$

28. $\mathrm{\neg }A\to (A\to B)$

29. $(\mathrm{\neg }A\vee B)\leftrightarrow (A\to B)$

30. $(\mathrm{\neg }A\vee B)\leftrightarrow (A\to B)$

31. $A\vee \mathrm{\perp }\leftrightarrow A$

32. $A\vee \mathrm{\perp }\leftrightarrow A$

33. $A\wedge \mathrm{\perp }\leftrightarrow \mathrm{\perp }$

34. $A\wedge \mathrm{\perp }\leftrightarrow \mathrm{\perp }$

35. $A\vee \mathrm{\neg }A$

36. $A\vee \mathrm{\neg }A$

37. $\mathrm{\neg }(A\leftrightarrow \mathrm{\neg }A)$

38. $\mathrm{\neg }(A\leftrightarrow \mathrm{\neg }A)$

39. $(A\to B)\leftrightarrow (\mathrm{\neg }B\to \mathrm{\neg }A)$

40. $(A\to B)\leftrightarrow (\mathrm{\neg }B\to \mathrm{\neg }A)$

41. $(A\to C\vee D)\to ((A\to C)\vee (A\to D))$

42. $(A\to C\vee D)\to ((A\to C)\vee (A\to D))$

43. $(((A\to B)\to A)\to A)$

44. $(((A\to B)\to A)\to A)$

所有这些都可以通过使用第 3.1 节中列出的基本规则在自然演绎中得出。但其中一些需要使用归谬法规则或反证法，我们尚未详细讨论过。我们将在第 5 章中讨论此规则的使用以及其他经典逻辑模式。

All of these can be derived in natural deduction using the fundamental rules listed in Section 3.1. But some of them require the use of the reductio ad absurdum rule, or proof by contradiction, which we have not yet discussed in detail. We will discuss the use of this rule, and other patterns of classical logic, in the Chapter 5.

3.6.练习¶

3.6. Exercises¶

在自然演绎中构建证明时，仅使用第 3.1 节中给出的规则列表。

When constructing proofs in natural deduction, use only the list of rules given in Section 3.1.

1. 给出自然演绎证明$A\wedge B$来自假设$B\wedge A$。

2. Give a natural deduction proof of $A\wedge B$ from hypothesis $B\wedge A$.

3. 给出自然演绎证明$(Q\to R)\to R$来自假设$Q$。

4. Give a natural deduction proof of $(Q\to R)\to R$ from hypothesis $Q$.

5. 给出自然演绎证明$\mathrm{\neg }(A\wedge B)\to (A\to \mathrm{\neg }B)$。

6. Give a natural deduction proof of $\mathrm{\neg }(A\wedge B)\to (A\to \mathrm{\neg }B)$.

7. 给出自然演绎证明$Q\wedge S$来自假设$(P\wedge Q)\wedge R$和$S\wedge T$。

8. Give a natural deduction proof of $Q\wedge S$ from hypotheses $(P\wedge Q)\wedge R$ and $S\wedge T$.

9. 给出自然演绎证明$(A\to C)\wedge (B\to \mathrm{\neg }C)\to \mathrm{\neg }(A\wedge B)$。

10. Give a natural deduction proof of $(A\to C)\wedge (B\to \mathrm{\neg }C)\to \mathrm{\neg }(A\wedge B)$.

11. 给出自然演绎证明$(A\wedge B)\to ((A\to C)\to \mathrm{\neg }(B\to \mathrm{\neg }C))$。

12. Give a natural deduction proof of $(A\wedge B)\to ((A\to C)\to \mathrm{\neg }(B\to \mathrm{\neg }C))$.

13. 再看一下上一章的练习 3。使用命题变量$A$，$B$， 和$C$分别针对“艾伦喜欢袋鼠”“贝蒂喜欢青蛙”和“卡尔喜欢仓鼠”这三个假设，将这三个假设表达为符号公式，然后通过自然演绎从中得出矛盾。

14. Take another look at Exercise 3 in the last chapter. Using propositional variables $A$, $B$, and $C$ for “Alan likes kangaroos,” “Betty likes frogs” and “Carl likes hamsters,” respectively, express the three hypotheses as symbolic formulas, and then derive a contradiction from them in natural deduction.

15. 给出自然演绎证明$A\vee B\to B\vee A$。

16. Give a natural deduction proof of $A\vee B\to B\vee A$.

17. 给出自然演绎证明$\mathrm{\neg }A\wedge \mathrm{\neg }B\to \mathrm{\neg }(A\vee B)$

18. Give a natural deduction proof of $\mathrm{\neg }A\wedge \mathrm{\neg }B\to \mathrm{\neg }(A\vee B)$

19. 给出自然演绎证明$\mathrm{\neg }(A\wedge B)$从$\mathrm{\neg }A\vee \mathrm{\neg }B$.（你不需要使用反证法。）

20. Give a natural deduction proof of $\mathrm{\neg }(A\wedge B)$ from $\mathrm{\neg }A\vee \mathrm{\neg }B$. (You do not need to use proof by contradiction.)

21. 给出自然演绎证明$\mathrm{\neg }(A\leftrightarrow \mathrm{\neg }A)$。

22. Give a natural deduction proof of $\mathrm{\neg }(A\leftrightarrow \mathrm{\neg }A)$.

23. 给出自然演绎证明$(\mathrm{\neg }A\leftrightarrow \mathrm{\neg }B)$来自假设$A\leftrightarrow B$。

24. Give a natural deduction proof of $(\mathrm{\neg }A\leftrightarrow \mathrm{\neg }B)$ from hypothesis $A\leftrightarrow B$.

25. 给出自然演绎证明$P\to R$来自假设$(P\vee Q)\to R$. 这与证明$((P\vee Q)\to R)\to (P\to R)$？

26. Give a natural deduction proof of $P\to R$ from hypothesis $(P\vee Q)\to R$. How does this differ from a proof of $((P\vee Q)\to R)\to (P\to R)$?

27. 给出自然演绎证明$C\to (A\vee B)\wedge C$来自假设$A\vee B$。

28. Give a natural deduction proof of $C\to (A\vee B)\wedge C$ from hypothesis $A\vee B$.

29. 给出自然演绎证明$W\vee Y\to X\vee Z$来自假设$W\to X$和$Y\to Z$。

30. Give a natural deduction proof of $W\vee Y\to X\vee Z$ from hypotheses $W\to X$ and $Y\to Z$.

31. 给出自然演绎证明$(A\vee (B\wedge A))\to A$。

32. Give a natural deduction proof of $(A\vee (B\wedge A))\to A$.

4.1.命题和证明的表达式¶

4.1. Expressions for Propositions and Proofs¶

从本质上讲，Lean 是一种类型检查器。这意味着我们可以编写表达式并要求系统检查它们是否格式正确，还可以要求系统告诉我们它们表示什么类型的对象。试试这个：

At its core, Lean is what is known as a type checker. This means that we can write expressions and ask the system to check that they are well formed, and also ask the system to tell us what type of object they denote. Try this:

variables A B C : Prop

#check A ∧ ¬ B → C

variables A B C : Prop

#check A ∧ ¬ B → C

在该文本的在线版本中，您可以按“试试看！”按钮将示例复制到编辑器窗口，然后将鼠标悬停在文本上的标记上以阅读消息。

In the online version of this text, you can press the “try it!” button to copy the example to an editor window, and then hover over the markers on the text to read the messages.

在示例中，我们声明了三个遍历命题的变量，并要求 Lean 检查表达式。该命令的输出是，它断言的类型为。在 Lean 中，每个格式正确的表达式都有一个类型。A ∧ ¬ B → C#checkA ∧ ¬ B → C : PropA ∧ ¬ B → CProp

In the example, we declare three variables ranging over propositions, and ask Lean to check the expression A ∧ ¬ B → C. The output of the #check command is A ∧ ¬ B → C : Prop, which asserts that A ∧ ¬ B → C is of type Prop. In Lean, every well-formed expression has a type.

逻辑连接词以 unicode 呈现。下表向您展示了如何在编辑器中输入这些符号，还为纯粹主义者提供了 ascii 等效符号。

The logical connectives are rendered in unicode. The following chart shows you how you can type these symbols in the editor, and also provides ascii equivalents, for the purists among you.

到目前为止，我们只讨论了列表中的前七项。稍后我们将讨论量词、lambda 和相等性。尝试输入一些表达式并自行检查。您应该尝试将上例中的一个变量更改为D，或在表达式中插入一个无意义的符号，然后查看 Lean 返回的错误消息。

So far, we have only talked about the first seven items on the list. We will discuss the quantifiers, lambda, and equality later. Try typing some expressions and checking them on your own. You should try changing one of the variables in the example above to D, or inserting a nonsense symbol into the expression, and take a look at the error message that Lean returns.

除了声明变量之外，如果P是任何类型的表达式，我们还可以声明为真的Prop假设：P

In addition to declaring variables, if P is any expression of type Prop, we can declare the hypothesis that P is true:

variables A B : Prop
variable  h : A ∧ ¬ B

#check h

variables A B : Prop
variable  h : A ∧ ¬ B

#check h

形式上，任何命题都可以看作是一种类型，即该命题的证明类型。假设或前提只是该类型的变量。然后，建立证明就是写下正确类型的表达式。例如，如果 是P类型的任何表达式，则是 类型的表达式，是 类型的表达式。换句话说，如果是 的证明， 是通过应用 和 的左消去规则得到的证明的名称：A ∧ Band.left PAand.right PBPA ∧ Band.left P

Formally, what is going on is that any proposition can be viewed as a type, namely, the type of proofs of that proposition. A hypothesis, or premise, is just a variable of that type. Building proofs is then a matter of writing down expressions of the correct type. For example, if P is any expression of type A ∧ B, then and.left P is an expression of type A, and and.right P is an expression of type B. In other words, if P is a proof of A ∧ B, and and.left P is a name for the proof you get by applying the left elimination rule for and:

类似地，是通过应用正确的消去规则得到的证明。因此，继续上面的例子，我们可以写and.right PB

Similarly, and.right P is the proof of B you get by applying the right elimination rule. So, continuing the example above, we can write

variables A B : Prop
variable h : A ∧ ¬ B

#check and.left h
#check and.right h

variables A B : Prop
variable h : A ∧ ¬ B

#check and.left h
#check and.right h

这两个表达式分别代表这两个证明：

The two expressions represent, respectively, these two proofs:

请注意，在这种表示自然演绎证明的方式中，没有“自由浮动”的假设。每个假设都有一个标签。在精益中，我们通常使用诸如h、h1、h2、 等表达式来标记假设，但您可以使用任何您想要的标识符。

Notice that in this way of representing natural deduction proofs, there are no “free floating” hypotheses. Every hypothesis has a label. In Lean, we will typically use expressions like h, h1, h2, … to label hypotheses, but you can use any identifier you want.

如果h1是 的证明A，h2是 的证明B， 则是 的证明。因此我们可以继续上面的例子：and.intro h1 h2A ∧ B

If h1 is a proof of A and h2 is a proof of B, then and.intro h1 h2 is a proof of A ∧ B. So we can continue the example above:

variables A B : Prop
variable h : A ∧ ¬ B

#check and.intro (and.right h) (and.left h)

variables A B : Prop
variable h : A ∧ ¬ B

#check and.intro (and.right h) (and.left h)

这对应于以下证明：

This corresponds to the following proof:

那么蕴涵呢？消去规则很简单：如果P₁是的证明，并且是的证明，那么就是的证明。请注意，我们甚至不需要命名规则：只需写下后跟，就好像您将第一个应用于第二个一样。如果和是复合表达式，请在它们周围加上括号，以明确每个表达式的开始和结束位置。A → BP₂AP₁ P₂BP₁P₂P₁P₂

What about implication? The elimination rule is easy: if P₁ is a proof of A → B and P₂ is a proof of A then P₁ P₂ is a proof of B. Notice that we do not even need to name the rule: you just write P₁ followed by P₂, as though you are applying the first to the second. If P₁ and P₂ are compound expressions, put parentheses around them to make it clear where each one begins and ends.

variables A B C D : Prop

variable h1 : A → (B → C)
variable h2 : D → A
variable h3 : D
variable h4 : B

#check h2 h3
#check h1 (h2 h3)
#check (h1 (h2 h3)) h4